apply funext
case zeroCoeff
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ (0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail') ≈ mulMonom b h tail ++ mul tail tail'
case zeroCoeff.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁ s₂ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ ∀ (x : G),
    coords ((0, g * h) :: (mulMonom b h tail ++ mul ((0, g) :: tail) tail')) x =
      coords (mulMonom b h tail ++ mul tail tail') x