proposition: Lemma logp_sum_floor p n : prime p -> logn p (n`!) = \sum_(i < trunc_log p n) n %/ p ^ i.+1.
proof: Proof. move=> hp; rewrite -fact_logp_sum_small //; apply: trunc_log_ltn. exact: prime_gt1. Qed.
imports: mathcomp(all_ssreflect all_algebra)