Leanパズル【問題編】スターリンソート

Lean4でスターリンソート（ソートになっていない部分を前から削除していく処理）を実装すると次のようになります。

open Std

variable {α : Type} [LE α] [DecidableLE α]

/-- ソートになっていない部分を前から削除していく関数。
（ソートと名前が付いているが厳密にはソートではない） -/
@[simp, grind]
def stalinSort (l : List α) : List α :=
  match l with
  | [] => []
  | [x] => [x]
  | x :: y :: xs =>
    if x ≤ y then
      x :: stalinSort (y :: xs)
    else
      stalinSort (x :: xs)

これについて、実際に出力結果がソート済みであることを証明してみましょう。

以下のsorryの部分を埋めて証明を完成させてください。ただし、必要に応じて補題を追加しても構いません。

variable [IsPreorder α]

theorem stalinSort_sorted (l : List α) : (stalinSort l).Pairwise (· ≤ ·) := by
  sorry