simp [coords, monom_coords_at_zero, ← add_assoc, monom_coords_hom]
case addCoeffs
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁ s₂ : FormalSum R X
a b : R
x : X
tail : FormalSum R X
⊢ coords ((a, x) :: (b, x) :: tail) x₀ = coords ((a + b, x) :: tail) x₀
no goals