rw [ih]
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 (tail ++ s₂)) x₀ = coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
⊢ monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h (tail ++ s₂)) x₀ =
    monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) 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 (tail ++ s₂)) x₀ = coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀
⊢ monomCoeff R G x₀ (head.1 * b, head.2 * h) + (coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀) =
    monomCoeff R G x₀ (head.1 * b, head.2 * h) + coords (mulMonom b h tail) x₀ + coords (mulMonom b h s₂) x₀