apply Nat.succ_lt_succ
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
c : (x == x₀) = false
k : R := coords tail x₀
pos : 0 ≠ k
lem : k = coords ((a, x) :: tail) x₀
ys' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
ys : List (R × X) := (a, x) :: ys'
⊢ Nat.succ (List.length ys') < Nat.succ (List.length tail)
case a
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
c : (x == x₀) = false
k : R := coords tail x₀
pos : 0 ≠ k
lem : k = coords ((a, x) :: tail) x₀
ys' : FormalSum R X
eqnStep : (coords tail x₀, x₀) :: ys' ≃ tail
lIneqStep : List.length ys' < List.length tail
ys : List (R × X) := (a, x) :: ys'
⊢ List.length ys' < List.length tail