proposition: Lemma T1le_mul2r x y z: (y <= z) -> (y * x <= z * x).
proof: Proof. by rewrite !T1leNgt; apply: contra; apply: T1lt_mul2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)