apply Or.intro_right
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ False ∨ length (split (x :: xs)).snd + 1 < length xs + 1 + 1 + 1
case h
α : Type u_1
x₁ x₂ x : α
xs : List α
ih : x :: xs = [] ∨ length (split (x :: xs)).snd < length (x :: xs)
⊢ length (split (x :: xs)).snd + 1 < length xs + 1 + 1 + 1