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⟩
case cons.true
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₀
c : (x == x₀) = true
k : R := coords tail x₀
lem : a + k = coords ((a, x₀) :: tail) x₀
c'' : x = x₀
⊢ ∃ ys, (coords ((a, x₀) :: tail) x₀, x₀) :: ys ≃ (a, x₀) :: tail ∧ List.length ys < List.length ((a, x₀) :: tail)
no goals