induction b with
| zero =>
  change a * (0 + c) = a * 0 + a * c
  rw [zero_add, mul_zero, zero_add]
| succ n hn =>
  rw [succ_add, mul_succ, hn, mul_succ, add_assoc, add_comm (a*c), add_assoc]
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (b + c) = a * b + a * c
no goals