proposition: Lemma fact_logp_sum_widen p m n : prime p -> (m >= n)%N -> logn p n`! = \sum_(i < m) (n %/ p ^ i.+1).
proof: Proof. move => prime_p leq_nm; rewrite logn_fact //; symmetry. pose G (i : nat) := n %/ p ^ i.+1. rewrite -[LHS](big_mkord (fun _ => true) G); rewrite {}/G. rewrite (big_cat_nat _ _ _ (leq0n n) leq_nm) /= addnC. rewrite big_nat_cond /= big1; first by rewrite add0n big_add1. move=> i; rewrite andbT => /andP [leni ltim]; apply: divn_small. apply: leq_trans (ltn_expl _ _); first exact: leq_trans leni _. exact: prime_gt1. Qed.
imports: mathcomp(all_ssreflect all_algebra)