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
21. 21
22. 22
23. 23

import Mathlib

variable [LinearOrder α] (xs : List α)

inductive Sorted' : List α → Prop where
  | nil : Sorted' []
  | single x : Sorted' [x]
  | cons_cons x x' xs : x ≤ x' → Sorted' (x' :: xs) → Sorted' (x :: x' :: xs)

-- open Classical in
-- noncomputable def List.insSort : List α := by
--   have blah' : ∃ ys : List α, Sorted' ys ∧ ys.Perm xs := by
--     sorry
--   have blah : ∃ n, 3 + n = 4 := by
--     use 1
--   obtain ⟨x, hx⟩ := blah
--   exact ys




theorem insSortCorrect : ∃ ys, Sorted' ys ∧ xs.Perm ys := by
  have : xs.permutations