proposition: Lemma T1le_mul2l x y z : x != zero -> T1nf y -> (x *y <= x *z) = (y <= z).
proof: Proof. by move => sa sn; rewrite !T1leNgt T1lt_mul2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)