add_factorial_succ_le_factorial_add_succ

English

For all i,n ∈ ℕ, i + (n+1)! ≤ (i+(n+1))!.

Русский

Для всех i,n ∈ ℕ: i + (n+1)! ≤ (i+(n+1))!.

LaTeX

$$$i,n \in \mathbb{N} \rightarrow i + (n+1)! \le (i+(n+1))!$$$

Lean4

theorem add_factorial_succ_le_factorial_add_succ (i : ℕ) (n : ℕ) : i + (n + 1)! ≤ (i + (n + 1))! :=
  by
  cases (le_or_gt (2 : ℕ) i)
  · rw [← Nat.add_assoc]
    apply Nat.le_of_lt
    apply add_factorial_succ_lt_factorial_add_succ
    assumption
  ·
    match i with
    | 0 => simp
    |
    1 =>
      rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n, Nat.add_le_add_iff_right]
      exact Nat.mul_pos n.succ_pos n.succ.factorial_pos
    | succ (succ n) => contradiction

Похожие утверждения