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

case succ
m n k : MyNat
ih : m.mul (n.add k) = (m.mul n).add (m.mul k)
⊢ m.mul (n.add k.succ) = (m.mul n).add (m.mul k.succ)