proposition: Lemma T1le_mulCE (m1:= one) (m2:= T1bad) (n1 := \F1) (n2 := one) : (m1 <= n1) && (m2 <= n2) && ( m1 * m2 <= n1 * n2) == false.
proof: Proof. done. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)