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

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

⊢ 0 * 0 = 0

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

State before:
case zero

⊢ 0 * 0 = 0
Tactic:
rw [mul_zero]
State after:
no goals

State before:
case succ
d : MyNat
hd : 0 * d = 0
⊢ 0 * succ d = 0
Tactic:
rw [mul_succ, hd, add_zero]
State after:
no goals