Theorem: Nat.lt_add (SetTheory/Formula.lean)

State before:
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
⊢ n < n + (m + 1)
Tactic:
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
State after:
no goals

State before:
case zero
V : Type ?u.7600
inst✝ : SetTheory V
n : Nat
⊢ n < n + (zero + 1)
Tactic:
rw [Nat.lt_succ]
State after:
case zero
V : Type ?u.7600
inst✝ : SetTheory V
n : Nat
⊢ n ≤ n

State before:
case zero
V : Type ?u.7600
inst✝ : SetTheory V
n : Nat
⊢ n ≤ n
Tactic:
exact Nat.le_refl n
State after:
no goals

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

State before:
case succ
V : Type ?u.7600
inst✝ : SetTheory V
n m : Nat
ih : n < n + (m + 1)
⊢ n ≤ n + succ m
Tactic:
exact Nat.le_of_lt ih
State after:
no goals