Theorem: MyNat.le_succ (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ a ≤ b → a ≤ succ b
Tactic:
intro
| ⟨ c, hc ⟩ =>
  exists succ c
  repeat (rw [succ_eq_add_one])
  rw [← add_assoc, hc]
State after:
no goals

State before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ a ≤ succ b
Tactic:
exists succ c
State after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ succ b = a + succ c

State before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ succ b = a + succ c
Tactic:
repeat (rw [succ_eq_add_one])
State after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)

State before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)
Tactic:
rw [← add_assoc, hc]
State after:
no goals

State before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + succ c
Tactic:
(rw [succ_eq_add_one])
State after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)

State before:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + succ c
Tactic:
rw [succ_eq_add_one]
State after:
a b : Nat
x✝ : a ≤ b
c : Nat
hc : b = a + c
⊢ b + one = a + (c + one)