rw [← append_coords]
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = coords (scmul a s₁ ++ scmul a s₂) x₀
case h.a.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a : R
x₁ x₂ : R[X]
s₁ s₂ : FormalSum R X
x₀ : X
⊢ a * (coords s₁ x₀ + coords s₂ x₀) = coords (scmul a s₁) x₀ + coords (scmul a s₂) x₀