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