induction c with
| zero =>
  change a + b + 0 = a + (b + 0)
  rw [add_zero, add_zero]
| succ c hrec =>
  rw [add_succ, add_succ, add_succ, hrec]
S : Type
image_zero : S
image_succ : N → S → S
n m a b c : N
⊢ a + b + c = a + (b + c)
no goals