match lst with
| x :: y :: xs =>
  simp_arith [splitList]
  apply splitList_shorter_le
α : Type u_1
lst : List α
x✝ : List.length lst ≥ 2
⊢ List.length (splitList lst).fst < List.length lst ∧ List.length (splitList lst).snd < List.length lst
no goals