simp [mulMonom, coords]
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ coords (mulMonom (b₁ + b₂) h ((a, g) :: tail)) x₀ =
    coords (mulMonom b₁ h ((a, g) :: tail)) x₀ + coords (mulMonom b₂ h ((a, g) :: tail)) x₀
case cons
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b₁ b₂ : R
h x₀ : G
head : R × G
tail : List (R × G)
ih : coords (mulMonom (b₁ + b₂) h tail) x₀ = coords (mulMonom b₁ h tail) x₀ + coords (mulMonom b₂ h tail) x₀
a : R
g : G
⊢ monomCoeff R G x₀ (a * (b₁ + b₂), g * h) + coords (mulMonom (b₁ + b₂) h tail) x₀ =
    monomCoeff R G x₀ (a * b₁, g * h) + coords (mulMonom b₁ h tail) x₀ +
      (monomCoeff R G x₀ (a * b₂, g * h) + coords (mulMonom b₂ h tail) x₀)