proposition: Lemma pfactorKpdiv p n : prime p -> logn (pdiv (p ^ n)) (p ^ n) = n.
proof: Proof. by case: n => // n p_pr; rewrite pdiv_pfactor ?pfactorK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)