proposition: Lemma part_pnat pi n : pi.-nat n`_pi.
proof: Proof. rewrite /pnat primes_part part_gt0. by apply/allP=> p; rewrite mem_filter => /andP[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)