induction a with
| zero =>
  change 0 * b = a * 0
  rw [zero_mul, mul_zero]
| succ n hn =>
  rw [succ_mul, hn, mul_succ]
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * b = b * a
no goals