induction t with
| zero =>
  rw [add_zero, add_zero]
  intro h
  exact h
| succ t' ih =>
  rw [add_succ, add_succ]
  intro h
  have ihl : a + t' = b + t' := by exact (succ_inj h)
  exact (ih ihl)
a b t : Nat
⊢ a + t = b + t → a = b
no goals