Theorem: MyNat.zero_add (IIScExperiments/Solutions/NatAddMulExperiments.lean)

State before:
a : MyNat
⊢ 0 + a = a
Tactic:
induction' a using MyNat.induction with d hd
State after:
case zero

⊢ 0 + 0 = 0

case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d

State before:
case zero

⊢ 0 + 0 = 0
Tactic:
rw [add_zero]
State after:
no goals

State before:
case succ
d : MyNat
hd : 0 + d = d
⊢ 0 + succ d = succ d
Tactic:
rw [add_succ, hd]
State after:
no goals