split proof reduction size

split.lean

def split [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)]
 : List a → (a × List a × List a)
 | []      => (default, [], [])
 | x :: xs =>
   let rec op x acc :=
    if x ≤ acc.1
    then (x, acc.1 :: acc.2.2, acc.2.1)
    else (acc.1, x :: acc.2.2, acc.2.1)
   xs.foldr op (x, [], [])

#eval split ([1,2,3,4,5] : List Nat)

theorem split_left_le [Inhabited a] [LE a] [DecidableRel (α := a) (· ≤ ·)]
 (xs : List a) : (split xs).2.1.length ≤ xs.length := by
  unfold split
  split ; simp
  rename_i x xs
  induction xs with
  | nil => simp [split]
  | cons y xs ih =>
    unfold List.foldr
    simp [split.op]
    split ; simp

    induction xs with
    | nil => simp [List.foldr_nil]
    | cons y ys ih₁ =>
      simp [List.foldr_cons]
      cases decide (x ≤ y) with
      | inl h =>
        simp [h]
        exact Nat.succ_le_succ ih
      | inr h =>
        simp [h]
        exact ih