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