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