assumption
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
_x✝ : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0
a✝¹ :
  ∀ (y : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0),
    (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1 y _x✝ → y.1 ≃ []
s : FormalSum R X
hyp✝¹ : ∀ (x : X), coords s x = 0
a✝ :
  ∀ (y : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0),
    (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1 y
        { fst := s, snd := hyp✝¹ } →
      y.1 ≃ []
h : R × X
t : List (R × X)
hyp✝ : ∀ (x : X), coords (h :: t) x = 0
mt✝ : s = h :: t
x✝¹ :
  ∀ (y : (s : FormalSum R X) ×' ∀ (x : X), coords s x = 0),
    (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1 y
        { fst := h :: t, snd := hyp✝ } →
      y.1 ≃ []
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = 0
mt : s = (a₀, x₀) :: t
hyp₀ : coords ((a₀, x₀) :: t) x₀ = 0 := hyp x₀
c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀
hz : ¬a₀ = 0
non_zero : 0 ≠ coords t x₀
ys : FormalSum R X
eqnStep : (coords t x₀, x₀) :: ys ≃ t
lIneqStep : List.length ys < List.length t
tail_coeffs : ∀ (x : X), coords ys x = 0
x✝ : List.length ys < List.length (h :: t)
⊢ (invImage (fun a => PSigma.casesOn a fun s snd => List.length s) instWellFoundedRelation).1
    { fst := ys, snd := tail_coeffs } { fst := h :: t, snd := hyp✝ }
no goals