proposition: Lemma dvdn_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
proof: Proof. by move=> /dvdnP[q1 ->] /dvdnP[q2 ->]; rewrite mulnCA -mulnA 2?dvdn_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)