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