proposition: Lemma pnatP pi n : n > 0 -> reflect (forall p, prime p -> p %| n -> p \in pi) (pi.-nat n).
proof: Proof. move=> n_gt0; rewrite /pnat n_gt0. apply: (iffP allP) => /= pi_n p => [pr_p p_n|]. by rewrite pi_n // mem_primes pr_p n_gt0. by rewrite mem_primes n_gt0 /=; case/andP; move: p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)