proposition: Lemma logn_count_dvd p n : prime p -> logn p n = \sum_(1 <= k < n) (p ^ k %| n).
proof: Proof. rewrite big_add1 => p_prime; case: n => [|n]; first by rewrite logn0 big_geq. rewrite big_mkord -big_mkcond (eq_bigl _ _ (fun _ => pfactor_dvdn _ _ _)) //=. by rewrite big_ord_narrow ?sum1_card ?card_ord // -ltnS ltn_logl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)