proposition: Lemma logn_part p m : logn p m`_p = logn p m.
proof: Proof. case p_pr: (prime p); first by rewrite p_part pfactorK. by rewrite lognE (lognE p m) p_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)