proposition: Lemma lcm_leq_Cnk n k : iter_lcmn n <= C n k.
proof: Proof. case: n => [|n]; first by rewrite iter_lcmn0 . set ln := iter_lcmn n.+1. suff Hdiv : ln %| C n.+1 k. exact: dvdn_leq => // . apply/dvdn_partP => [|p Hp]; first by (rewrite iter_lcmn_gt0). have Hprime : prime p by move: Hp; rewrite mem_primes; case/andP. suff Hlogntrunc: logn p ln <= logn p (C n.+1 k). by rewrite p_part pfactor_dvdn. suff lelogtrunc : logn p ln <= trunc_log p n.+1. exact: leq_trans (Hanson_2 _ _ _). apply: trunc_log_max; first by rewrite prime_gt1. suff Hj : {j | (j <= n.+1) && (ln`_p == j`_p)}. case: Hj => j /andP [Hj1 /eqP]; rewrite p_part => ->. case: j Hj1 => [|j Hj1]; first by rewrite partn0. exact/leq_trans/Hj1/dvdn_leq/dvdn_part. exact: part_p_iter_lcmn. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial