induction b with
| zero => rfl
| succ n hn =>
  rw [mul_succ, mul_succ, hn, add_assoc, add_assoc, add_succ,
    add_succ, add_succ, add_succ, add_comm n a]
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ succ a * b = a * b + b
no goals