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