induction' n with n ih
m n : MyNat
⊢ m.succ.add n = (m.add n).succ
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