simp [mulMonom, coords]
case swap
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ : FormalSum R G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
⊢ coords (mulMonom b h ((a₁, x₁) :: (a₂, x₂) :: tail)) x₀ = coords (mulMonom b h ((a₂, x₂) :: (a₁, x₁) :: tail)) x₀
case swap
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ : FormalSum R G
a₁ a₂ : R
x₁ x₂ : G
tail : FormalSum R G
⊢ monomCoeff R G x₀ (a₁ * b, x₁ * h) + (monomCoeff R G x₀ (a₂ * b, x₂ * h) + coords (mulMonom b h tail) x₀) =
    monomCoeff R G x₀ (a₂ * b, x₂ * h) + (monomCoeff R G x₀ (a₁ * b, x₁ * h) + coords (mulMonom b h tail) x₀)