proposition: Lemma Euclid_dvdM m n p : prime p -> (p %| m * n) = (p %| m) || (p %| n).
proof: Proof. move=> pr_p; case dv_pm: (p %| m); first exact: dvdn_mulr. by rewrite Gauss_dvdr // prime_coprime // dv_pm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)