induction xs with
| nil =>
  intro n
  rfl
| cons y ys ih =>
  intro n
  simp [NonTail.sum, Tail.sumHelper]
  rw [← Nat.add_assoc, Nat.add_comm y n]
  exact ih (n + y)
xs : List Nat
⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
no goals