proposition: Lemma fact_logp_sum p n : prime p -> logn p n`! = \sum_(i < n) (n %/ p ^ i.+1).
proof: Proof. elim: n => [|n ihn] p_prime; first by rewrite fact0 logn1 big_ord0. rewrite factS lognM ?fact_gt0 // big_ord_recr /= ihn //=. rewrite divn_small ?addn0; last by rewrite ltn_expl ?prime_gt1. have -> : logn p n.+1 = \sum_(i < n) (p ^ i.+1 %| n.+1). rewrite -big_mkcond sum1dep_card; set P := [set x | _]. have -> : P = [set i : 'I__ | i.+1 <= logn p n.+1]. apply/setP => i; rewrite !inE /= -{1}(@partnC p n.+1) //. rewrite Gauss_dvdl; first by rewrite p_part dvdn_Pexp2l ?prime_gt1. by rewrite (@pnat_coprime p) ?part_pnat ?pnatX ?pnat_id. rewrite -sum1dep_card big_ord_narrow ?sum_nat_const ?muln1 ?card_ord //. rewrite -(@leq_exp2l p) ?prime_gt1 // -p_part. by rewrite (leq_trans (dvdn_leq _ (dvdn_part p _))) // ltn_expl ?prime_gt1. rewrite -big_split; apply: eq_big => //= i _; set q := p ^ i.+1; symmetry. have q_gt0 : 0 < q by rewrite ?expn_gt0 ?prime_gt0. rewrite {1}(divn_eq n q) -addn1 -addnA divnMDl // addnC addn1. have -> // : (q %| n.+1) = ((n %% q).+1 == q). rewrite -{3}[q]prednK // eqSS. by rewrite -(@modn_small q.-1 q) -1?(@eqn_modDr 1) ?addn1 prednK // modnn. have [->|hi] := altP eqP; first by rewrite divnn q_gt0. by rewrite divn_small // ltn_neqAle hi ltn_mod. Qed.
imports: mathcomp(all_ssreflect all_algebra)