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

case step
m n i h : ℕ
a✝ : Nat.le 1 h
⊢ i + (succ h)! ≤ (i + succ h)!
m n✝ i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!
cases' n1 with h
no goals
case step
m n i h : ℕ
a✝ : Nat.le 1 h
⊢ i + (succ h)! ≤ (i + succ h)!
exact add_factorial_succ_le_factorial_add_succ i h
no goals
case refl
m n i : ℕ
⊢ i + 1! ≤ (i + 1)!
exact self_le_factorial _