case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!

case step
m n i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + (succ m✝)! < (i + succ m✝)!
m n✝ i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
⊢ i + n ! < (i + n)!
cases hn
no goals
case step
m n i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + (succ m✝)! < (i + succ m✝)!
exact add_factorial_succ_lt_factorial_add_succ _ hi
case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!
case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!
rw [factorial_one]
no goals
case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!
exact lt_factorial_self (succ_le_succ hi)