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

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

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

State before:
case zero
a : MyNat
⊢ a + 0 = 0 + a
Tactic:
rw [add_zero, zero_add]
State after:
no goals

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