rw [← Nat.add_assoc, Nat.lt_succ]
case succ
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
ih : n < n + (m + 1)
⊢ n < n + (succ m + 1)
case succ
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
ih : n < n + (m + 1)
⊢ n ≤ n + succ m