1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20

import Mathlib.Order.Lattice

variable [LinearOrder α] (xs : List α)

@[grind]
def ins (a : α)
  | [] => [a]
  | x :: xs => if a ≤ x then a :: x :: xs else x :: ins a xs

abbrev List.insSort := xs.foldr ins []

abbrev Sorted := xs.IsChain (· ≤ ·)

theorem insCorrect x : (Sorted xs → Sorted (ins x xs)) ∧ (x :: xs).Perm (ins x xs) := by
  induction xs with
  | nil => grind
  | cons _ xs => cases xs <;> grind

theorem insSortCorrect : Sorted xs.insSort ∧ xs.Perm xs.insSort := by
  induction xs <;> grind [insCorrect]