equation lemma ugliness

Stream: general

[Kevin Buzzard]

def poly := list ℤ

def poly.add : poly → poly → poly
| [] g := g
| f [] := f
| (a :: f') (b :: g') := (a + b) :: poly.add f' g'

-- example (p : poly) : poly.add [] p = p := rfl -- fails

#print prefix poly.add

/-
...
poly.add.equations._eqn_1 : poly.add list.nil list.nil = list.nil
poly.add.equations._eqn_2 : ∀ (hd : ℤ) (tl : list ℤ), poly.add list.nil (hd :: tl) = hd :: tl
...

-- it did unnecessary cases on g.
-/

example (p : poly) : poly.add [] p = p := by cases p;refl

[Kevin Buzzard]

Is this just "one of those things" -- is my proof of poly.add using cases something which I should be OK with, or should I now start tweaking things to try and make the example rfl? I am about to make it a simp lemma -- is that "good enough"? As you can see, I can prove the result, I am just worried about whether my proof is somehow bad style. It's my fancy recursive definition which is to blame of course, but the definition is recursive (I'm representing a polynomial as a list of its coefficients starting with the constant term)