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