induction s with
| nil =>
  simp [scmul]
  apply eqlCoords.refl
| cons h t ih =>
  apply funext; intro x₀
  let il₁ := congrFun ih x₀    
  rw [← append_coords]
  simp [scmul, coords, right_distrib, monom_coords_hom]
  rw [← append_coords] at il₁ 
  rw [← il₁]
  conv =>
    lhs
    rw [add_assoc]
    arg 2
    rw [← add_assoc]
    arg 1
    rw [add_comm]
  conv =>
    lhs
    rw [add_assoc]
    rw [← add_assoc]
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
s : FormalSum R X
⊢ scmul a s ++ scmul b s ≈ scmul (a + b) s
no goals