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