induction s₂ with
| nil => 
  simp [mulMonom, coords]
| cons head tail ih =>
  let (a, x) := head
  simp [mulMonom, coords, mul]
  rw [← append_coords]
  rw [mul_monom_dist]
  rw [ih]
  simp [add_assoc, mulMonom]
  rw [mul_monom_monom_assoc]
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
b : R
h x₀ : G
s₁ s₂ : FormalSum R G
⊢ coords (mulMonom b h (mul s₁ s₂)) x₀ = coords (mul s₁ (mulMonom b h s₂)) x₀
no goals