simp [mulMonom, coords,monom_coords_at_zero]
case zeroCoeff
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ tail : FormalSum R G
g : G
a : R
hyp : a = 0
⊢ coords (mulMonom b h ((0, g) :: tail)) x₀ = coords (mulMonom b h tail) x₀
no goals