induction' n with n ih
m n : MyNat
⊢ m.succ.mul n = (m.mul n).add n
case zero
m : MyNat
⊢ m.succ.mul zero = (m.mul zero).add zero

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