simp [mul]
case addCoeffs
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
a₁ a₂ : R
x : G
tail : FormalSum R G
⊢ mul ((a₁, x) :: (a₂, x) :: tail) ((b, h) :: tail') ≈ mul ((a₁ + a₂, x) :: tail) ((b, h) :: tail')
case addCoeffs
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
a₁ a₂ : R
x : G
tail : FormalSum R G
⊢ mulMonom b h ((a₁, x) :: (a₂, x) :: tail) ++ mul ((a₁, x) :: (a₂, x) :: tail) tail' ≈
    mulMonom b h ((a₁ + a₂, x) :: tail) ++ mul ((a₁ + a₂, x) :: tail) tail'