induction s with
| nil =>
  simp [scmul]
| cons h t ih =>
  simp [scmul, ih, mul_assoc]
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
s : FormalSum R X
⊢ scmul a (scmul b s) = scmul (a * b) s
no goals