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

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

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

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

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