proposition: Lemma leib_line n i k : lcmn 'L(n.+1, i) (\lcm_(j < k) 'L(n, i + j)) = \lcm_(j < k.+1) 'L(n.+1, i + j).
proof: Proof. elim: k i => [i|k1 IH i]. by rewrite big_ord_recr !big_ord0 /= lcmn1 lcm1n addn0. rewrite big_ord_recl /= addn0. rewrite lcmnA leibn_lcm_swap. rewrite (eq_bigr (fun j : 'I_k1 => 'L(n, i.+1 + j))). rewrite -lcmnA. rewrite IH. rewrite [RHS]big_ord_recl. rewrite addn0; congr (lcmn _ _). by apply: eq_bigr => j _; rewrite addnS. move=> j _. by rewrite addnS. Qed.
imports: mathcomp(all_ssreflect)