proposition: Lemma p_part_eq1 p n : (n`_p == 1) = (p \notin \pi(n)).
proof: Proof. rewrite mem_primes p_part lognE; case: and3P => // [[p_pr _ _]]. by rewrite -dvdn1 pfactor_dvdn // logn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)