induction m with
| zero =>
    rw [Nat.lt_succ]
    exact Nat.le_refl n
| succ m ih =>
    rw [← Nat.add_assoc, Nat.lt_succ]
    exact Nat.le_of_lt ih
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
⊢ n < n + (m + 1)
no goals