simp [mulMonom, coords, step]
case cons
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
a : R
x : G
t₁ t₂ : FormalSum R G
a✝ : ElementaryMove R G t₁ t₂
step : coords (mulMonom b h t₁) x₀ = coords (mulMonom b h t₂) x₀
⊢ coords (mulMonom b h ((a, x) :: t₁)) x₀ = coords (mulMonom b h ((a, x) :: t₂)) x₀
no goals