simp [mulMonom, coords, right_distrib, monom_coords_hom, add_assoc]
case addCoeffs
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 : G
tail : FormalSum R G
⊢ coords (mulMonom b h ((a₁, x) :: (a₂, x) :: tail)) x₀ = coords (mulMonom b h ((a₁ + a₂, x) :: tail)) x₀
no goals