add_factorial_succ_lt_factorial_add_succ

English

For all i,n ∈ ℕ with i ≥ 2, i + (n+1)! < (i+n+1)!.

Русский

Для всех i,n ∈ ℕ при i ≥ 2 выполняется: i + (n+1)! < (i+n+1)!.

LaTeX

$$$i \ge 2 \rightarrow i + (n+1)! < (i+n+1)!$$$

Lean4

theorem add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) : i + (n + 1)! < (i + n + 1)! :=
  by
  rw [factorial_succ (i + _), Nat.add_mul, Nat.one_mul]
  have := (i + n).self_le_factorial
  refine
      Nat.add_lt_add_of_lt_of_le (Nat.lt_of_le_of_lt ?_ ((Nat.lt_mul_iff_one_lt_right ?_).2 ?_)) (factorial_le ?_) <;>
    omega

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