proposition: Lemma Gauss_dvd m n p : coprime m n -> (m * n %| p) = (m %| p) && (n %| p).
proof: Proof. by move=> co_mn; rewrite -muln_lcm_gcd (eqnP co_mn) muln1 dvdn_lcm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)