proposition: Lemma mem_primes p n : (p \in primes n) = [&& prime p, n > 0 & p %| n].
proof: Proof. rewrite andbCA; have [-> // | /= n_gt0] := posnP. apply/mapP/andP=> [[[q e]]|[pr_p]] /=. case/mem_prime_decomp=> pr_q e_gt0 /dvdnP [u ->] -> {p}. by rewrite -(prednK e_gt0) expnS mulnCA dvdn_mulr. rewrite [n in _ %| n]prod_prime_decomp // big_seq. apply big_ind => [| u v IHu IHv | [q e] /= mem_qe dv_p_qe]. - by rewrite Euclid_dvd1. - by rewrite Euclid_dvdM // => /orP[]. exists (q, e) => //=; case/mem_prime_decomp: mem_qe => pr_q _ _. by rewrite Euclid_dvdX // dvdn_prime2 // in dv_p_qe; case: eqP dv_p_qe. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)