proposition: Lemma ltn_mul m1 m2 n1 n2 : m1 < n1 -> m2 < n2 -> m1 * m2 < n1 * n2.
proof: Proof. move=> lt_mn1 lt_mn2; apply (@leq_ltn_trans (m1 * n2)). by rewrite leq_mul2l orbC ltnW. by rewrite ltn_pmul2r // (leq_trans _ lt_mn2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring