cases c : x == x₀ with
| true =>
  let k := FormalSum.coords tail x₀
  have lem : a + k = coords ((a, x) :: tail) x₀ := by
    rw [coords, monomCoeff, c]
  have c'' : x = x₀ := of_decide_eq_true c
  rw [c'']
  rw [c''] at lem
  exact
    if c' : (0 = k) then by
      have lIneq : tail.length < List.length ((a, x) :: tail) := by
        simp [List.length_cons]
      rw [← c', add_zero] at lem
      rw [← lem]
      exact ⟨tail, rfl, lIneq⟩
    else by
      let ⟨ys, eqnStep, lIneqStep⟩ := hyp c'
      have eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys := by
        apply Quot.sound
        apply ElementaryMove.addCoeffs
      have eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail := by
        apply cons_equiv_of_equiv
        assumption
      have eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail := Eq.trans (Eq.symm eqn₁) eqn₂
      rw [← lem]
      have lIneq : ys.length < List.length ((a, x₀) :: tail) := by
        apply Nat.le_trans lIneqStep
        simp [List.length_cons, Nat.le_succ]
      exact ⟨ys, eqn, lIneq⟩
| false =>
  let k := coords tail x₀
  have lem : k = coords ((a, x) :: tail) x₀ := by
    simp [coords, monomCoeff, c, zero_add]
  rw [← lem] at pos
  let ⟨ys', eqnStep, lIneqStep⟩ := hyp pos
  rw [← lem]
  let ys := (a, x) :: ys'
  have lIneq : ys.length < ((a, x) :: tail).length := by
    simp [List.length_cons]
    apply Nat.succ_lt_succ
    exact lIneqStep
  have eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys' := by
    apply Quot.sound
    apply ElementaryMove.swap
  have eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail := by
    apply cons_equiv_of_equiv
    assumption
  have eqn : (k, x₀) :: ys ≃ (a, x) :: tail := by
    exact Eq.trans eqn₁ eqn₂
  exact ⟨ys, eqn, lIneq⟩
case cons
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
head : R × X
tail : List (R × X)
hyp : 0 ≠ coords tail x₀ → ∃ ys, (coords tail x₀, x₀) :: ys ≃ tail ∧ List.length ys < List.length tail
a : R
x : X
pos : 0 ≠ coords ((a, x) :: tail) x₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
no goals