intro x₀
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
⊢ ∀ (x : X), coords (scmul 0 s) x = coords [] x
case a.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x : R[X]
s : FormalSum R X
x₀ : X
⊢ coords (scmul 0 s) x₀ = coords [] x₀