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