simp [mulMonom, coords]
case nil
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₂ : FormalSum R G
⊢ coords (mulMonom b h ([] ++ s₂)) x₀ = coords (mulMonom b h []) x₀ + coords (mulMonom b h s₂) x₀
no goals