have c'' : x = x₀ := of_decide_eq_true c
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₀
⊢ ∃ ys, (coords ((a, x) :: tail) x₀, x₀) :: ys ≃ (a, x) :: tail ∧ List.length ys < List.length ((a, x) :: tail)
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)