proposition: Lemma pi_pdiv n : (pdiv n \in \pi(n)) = (n > 1).
proof: Proof. case: n => [|[|n]] //; rewrite /pdiv !inE /primes. have:= prod_prime_decomp (ltn0Sn n.+1); rewrite unlock. by case: prime_decomp => //= pf pd _; rewrite mem_head. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)