proposition: Lemma p_part p n : n`_p = p ^ logn p n.
proof: Proof. case (posnP (logn p n)) => [log0 |]. by rewrite log0 [n`_p]big1_seq // => q /andP [/eqP ->]; rewrite log0. rewrite logn_gt0 mem_primes; case/and3P=> _ n_gt0 dv_p_n. have le_p_n: p < n.+1 by rewrite ltnS dvdn_leq. by rewrite [n`_p]big_mkord (big_pred1 (Ordinal le_p_n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)