Theorem: MyNat.succ_add (MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
m n : MyNat
⊢ m.succ.add n = (m.add n).succ
Tactic:
induction' n with n ih
State after:
case zero
m : MyNat
⊢ m.succ.add zero = (m.add zero).succ

case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ m.succ.add n.succ = (m.add n.succ).succ

State before:
case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ m.succ.add n.succ = (m.add n.succ).succ
Tactic:
rw [add, ih]
State after:
case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ (m.add n).succ.succ = (m.add n.succ).succ

State before:
case succ
m n : MyNat
ih : m.succ.add n = (m.add n).succ
⊢ (m.add n).succ.succ = (m.add n.succ).succ
Tactic:
rfl
State after:
no goals

State before:
case zero
m : MyNat
⊢ m.succ.add zero = (m.add zero).succ
Tactic:
rfl
State after:
no goals