proposition: Lemma fact_logp_sum_small p j n : prime p -> (n < p ^ j.+1) -> logn p n`! = \sum_(i < j) (n %/ p ^ i.+1).
proof: Proof. move => prime_p leq_npj. case: (ltnP j n) => [le_jn|lt_nj]; last by rewrite (@fact_logp_sum_widen p j). rewrite logn_fact //. have hl : 1 <= j.+1 by []. have hr : j.+1 <= n.+1 by exact: ltnW. rewrite (big_cat_nat _ _ _ hl hr) /= addnC big_nat_cond /= big1. by rewrite add0n big_add1 /= big_mkord. move=> i; rewrite andbT => /andP [leni ltim]; apply: divn_small. apply: leq_trans leq_npj _; rewrite leq_exp2l //; exact: prime_gt1. Qed.
imports: mathcomp(all_ssreflect all_algebra)