Theorem: MyNat.zero_add (Talk/06Induction.lean)

State before:
m : MyNat
⊢ 0 + m = m
Tactic:
induction m with
| zero => dsimp
| succ m ih =>
  dsimp
  rw [ih]
State after:
no goals

State before:
case zero

⊢ 0 + zero = zero
Tactic:
dsimp
State after:
no goals

State before:
case succ
m : MyNat
ih : 0 + m = m
⊢ 0 + succ m = succ m
Tactic:
dsimp
State after:
case succ
m : MyNat
ih : 0 + m = m
⊢ 0 + m + 1 = m + 1

State before:
case succ
m : MyNat
ih : 0 + m = m
⊢ 0 + m + 1 = m + 1
Tactic:
rw [ih]
State after:
no goals