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