Theorem: MyNat.add_assoc (Talk/06Induction.lean)

State before:
m n o : MyNat
⊢ m + (n + o) = m + n + o
Tactic:
induction o with
| zero => simp
| succ o ih => simp [ih]
State after:
no goals

State before:
case zero
m n : MyNat
⊢ m + (n + zero) = m + n + zero
Tactic:
simp
State after:
no goals

State before:
case succ
m n o : MyNat
ih : m + (n + o) = m + n + o
⊢ m + (n + succ o) = m + n + succ o
Tactic:
simp [ih]
State after:
no goals