Theorem: LoVe.BackwardProofs.add_succ (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
m n : ℕ
⊢ add (Nat.succ m) n = Nat.succ (add m n)
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp [add, ih]
State after:
no goals

State before:
case zero
m : ℕ
⊢ add (Nat.succ m) Nat.zero = Nat.succ (add m Nat.zero)
Tactic:
rfl
State after:
no goals

State before:
case succ
m n' : ℕ
ih : add (Nat.succ m) n' = Nat.succ (add m n')
⊢ add (Nat.succ m) (Nat.succ n') = Nat.succ (add m (Nat.succ n'))
Tactic:
simp [add, ih]
State after:
no goals