induction rel with
| zeroCoeff tail g a hyp => 
  rw [hyp]
  simp [mulMonom, coords,monom_coords_at_zero]
| addCoeffs a₁ a₂ x tail => 
  simp [mulMonom, coords, right_distrib, monom_coords_hom, add_assoc]
  
| cons a x t₁ t₂ _ step => 
  simp [mulMonom, coords, step]
| swap a₁ a₂ x₁ x₂ tail => 
  simp [mulMonom, coords]
  conv =>
    lhs
    rw [← add_assoc]
    arg 1
    rw [add_comm]
  rw [← add_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
rel : ElementaryMove R G s₁ s₂
⊢ coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀
no goals