proposition: Lemma part_p_iter_lcmn_trunc_log p (Hprime : prime p) n : (iter_lcmn n)`_p = p ^ trunc_log p n.
proof: Proof. wlog: / 0 < n => [|n_gt0]. move => Hn. case: n Hn => // [|n ihn]. move => _; by rewrite iter_lcmn0 partn1 trunc_logn0 expn0. exact :ihn. have p_gt1 : 1 < p by exact: prime_gt1. have p_gt0 : 0 < p by exact: prime_gt0. suff H2ineq : (iter_lcmn n)`_p <= p ^ trunc_log p n /\ p ^ trunc_log p n <= (iter_lcmn n)`_p. apply: anti_leq; apply/andP; split; by case: H2ineq. split. - case: (part_p_iter_lcmn Hprime n) => j /andP [lejn /eqP lcmnpj]. case: j lejn lcmnpj => [|j] lejn lcmnpj. by rewrite lcmnpj partn0 expn_gt0 p_gt0. rewrite lcmnpj p_part. exact/leq_pexp2l/leq_logn_trunc. - apply/dvdn_leq/partp_dvdn/iter_lcmn_div/trunc_logP => //. by rewrite expn_gt0 p_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial