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

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

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

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