rw [← append_coords]
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords ([] ++ x) x₀ = coords x x₀
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x✝ : R[X]
x : FormalSum R X
x₀ : X
⊢ coords [] x₀ + coords x x₀ = coords x x₀