rw [Nat.add_assoc (length xs),
    Nat.add_assoc (length (split xs).1),
    Nat.add_comm 1,
    Nat.add_assoc (length (split xs).2),
    ←Nat.add_assoc (length (split xs).1)]
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + 1 + (length (split xs).snd + 1) = length xs + 1 + 1
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)