Theorem: MyNat.add_assoc (IIScExperiments/NatAddMul.lean)

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

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

State before:
case zero
a b : MyNat
⊢ a + b + 0 = a + (b + 0)
Tactic:
rfl
State after:
no goals

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

State before:
case succ
a b d : MyNat
hd : a + b + d = a + (b + d)
⊢ succ (a + (b + d)) = a + (b + succ d)
Tactic:
rfl
State after:
no goals