proposition: Lemma part_p_iter_lcmn p (Hprime : prime p) n : {j : nat | (j <= n) && ((iter_lcmn n)`_p == j`_p)}.
proof: Proof. elim: n => [|n ihn]. by exists 0; rewrite leqnn iter_lcmn0 partn0 partn1. case: ihn => j /andP [lejn] /eqP ihn. have H1 m : (iter_lcmn m)`_p = \big[lcmn/1]_(1 <= i < m.+1) i`_p. by rewrite /iter_lcmn !big_add1 /= 2!big_mkord partn_biglcm. have {H1} H2 : (iter_lcmn n.+1)`_p = lcmn j`_p n.+1`_p. rewrite H1 big_add1 big_nat_recr // -ihn /=; congr lcmn. by rewrite H1 big_add1 /= . have {H2}-> : (iter_lcmn n.+1)`_p = if logn p j < logn p n.+1 then n.+1`_p else j`_p. by rewrite H2 2!p_part -expn_max /maxn; case: ifP. case : ifP. by exists n.+1; rewrite ltnS leqnn eq_refl. by exists j; rewrite (leqW lejn) eq_refl. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial