proposition: Lemma lcm_lbound n : 2^n.-1 <= \lcm_(i < n) i.+1.
proof: Proof. case: n => [|n /=]; first by rewrite big_ord0. have <-: \lcm_(i < n.+1) 'L(i, 0) = \lcm_(i < n.+1) i.+1. by apply: eq_bigr => i _; rewrite leibn0. rewrite leib_corner. have -> : forall j, \lcm_(i < j.+1) 'L(n, i) = n.+1 * \lcm_(i < j.+1) 'C(n, i). elim=> [|j IH]; first by rewrite !big_ord_recr !big_ord0 /= !lcm1n. by rewrite big_ord_recr [in RHS]big_ord_recr /= IH muln_lcmr. rewrite (expnDn 1 1) /= (eq_bigr (fun i : 'I_n.+1 => 'C(n, i))) => [|i _]; last by rewrite !exp1n !muln1. have <- : forall n m, \sum_(i < n) m = n * m. by move=> m1 n1; rewrite sum_nat_const card_ord. apply: leq_sum => i _. apply: dvdn_leq; last by rewrite (bigD1 i) //= dvdn_lcml. apply big_ind => // [x y Hx Hy|x H]; first by rewrite lcmn_gt0 Hx. by rewrite bin_gt0 -ltnS. Qed.
imports: mathcomp(all_ssreflect)