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