rw [mul_monom_dist]
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁ ++ mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ : FormalSum R G
head : R × G
tail : List (R × G)
ih : coords (mulMonom b h (mul s₁ tail)) x₀ = coords (mul s₁ (mulMonom b h tail)) x₀
a : R
x : G
⊢ coords (mulMonom b h (mulMonom a x s₁)) x₀ + coords (mulMonom b h (mul s₁ tail)) x₀ =
    coords (mulMonom (a * b) (x * h) s₁) x₀ + coords (mul s₁ (mulMonom b h tail)) x₀