1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7

import Mathlib.Data.List.Sort

notation "insSort" => List.insertionSort (· ≤ ·)

theorem insSortCorrect [LinearOrder α] (xs : List α)
    : (insSort xs).SortedLE ∧ (insSort xs).Perm xs :=
  ⟨xs.sortedLE_insertionSort, xs.perm_insertionSort (· ≤ ·)⟩