simp only [split, length]
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ length (split (x₁ :: x₂ :: xs)).snd ≤ length (x₁ :: x₂ :: xs)
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).snd ≤ length xs
⊢ length (split xs).snd + 1 ≤ length xs + 1 + 1