simp [scmul, ih, mul_assoc]
case cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_2
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a (scmul b t) = scmul (a * b) t
⊢ scmul a (scmul b (h :: t)) = scmul (a * b) (h :: t)
no goals