proposition: Lemma T1eq_mul2l p m n : p != zero -> T1nf m -> T1nf n -> (p * m == p * n) = (m == n).
proof: Proof. move => sa sb sc; rewrite ! T1eq_le ! T1le_mul2l => //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)