induction s with
| nil =>
  intro contra
  contradiction
| cons head tail hyp =>
  let (a, x) := head
  intro pos
  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⟩
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s : FormalSum R X
⊢ 0 ≠ coords s x₀ → ∃ ys, (coords s x₀, x₀) :: ys ≃ s ∧ List.length ys < List.length s
no goals