proposition: Lemma pfactorK p n : prime p -> logn p (p ^ n) = n.
proof: Proof. move=> p_pr; have pn_gt0: p ^ n > 0 by rewrite expn_gt0 prime_gt0. apply/eqP; rewrite eqn_leq -pfactor_dvdn // dvdnn andbT. by rewrite -(leq_exp2l _ _ (prime_gt1 p_pr)) dvdn_leq // pfactor_dvdn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)