intro x₀
case cons.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁✝ s₂✝ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
⊢ ∀ (x_1 : G),
    coords (mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail') x_1 =
      coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x_1
case cons.h
R : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
G : Type
inst✝¹ : Group G
inst✝ : DecidableEq G
s₁✝ s₂✝ : FormalSum R G
head' : R × G
tail' : List (R × G)
b : R
h : G
a : R
x : G
s₁ s₂ : FormalSum R G
r : ElementaryMove R G s₁ s₂
a_ih✝ : mul s₁ ((b, h) :: tail') ≈ mul s₂ ((b, h) :: tail')
x₀ : G
⊢ coords (mulMonom b h ((a, x) :: s₁) ++ mul ((a, x) :: s₁) tail') x₀ =
    coords (mulMonom b h ((a, x) :: s₂) ++ mul ((a, x) :: s₂) tail') x₀