proposition: Lemma T1le_mul m1 m2 n1 n2 : T1nf m2 -> m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2.
proof: Proof. move => nm2 s1 s2;apply (@T1le_trans (m1 * n2)). case az: (m1==zero);first by rewrite (eqP az) ! T1mul0n. by rewrite T1le_mul2l // az. by apply:T1le_mul2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)