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

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

State before:
case zero

⊢ add 0 Nat.zero = Nat.zero
Tactic:
rfl
State after:
no goals

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