Theorem: MyNat.zero_add (MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
n : MyNat
⊢ zero.add n = n
Tactic:
induction' n with n ih
State after:
case zero

⊢ zero.add zero = zero

case succ
n : MyNat
ih : zero.add n = n
⊢ zero.add n.succ = n.succ

State before:
case succ
n : MyNat
ih : zero.add n = n
⊢ zero.add n.succ = n.succ
Tactic:
rw [add, ih]
State after:
no goals

State before:
case zero

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