apply Nat.lt.step
case h.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : length (split (x :: xs)).snd < Nat.succ (length xs)
⊢ length (split (x :: xs)).snd < length xs + 2
case h.a.a
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : length (split (x :: xs)).snd < Nat.succ (length xs)
⊢ length (split (x :: xs)).snd < length xs + 1