proposition: Lemma primesM m n p : m > 0 -> n > 0 -> (p \in primes (m * n)) = (p \in primes m) || (p \in primes n).
proof: Proof. move=> m_gt0 n_gt0; rewrite !mem_primes muln_gt0 m_gt0 n_gt0. by case pr_p: (prime p); rewrite // Euclid_dvdM. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)