apply Nat.le.step
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst + 1 ≤ length xs + 1 + 1
case a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ Nat.le (length (split xs).fst + 1) (length xs + 1)