proposition: Lemma pi_of_part pi n : n > 0 -> \pi(n`_pi) =i [predI \pi(n) & pi].
proof: Proof. by move=> n_gt0 p; rewrite /pi_of primes_part mem_filter andbC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)