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

@[simp]
instance : LE α := ⟨fun _ _ ↦ True⟩

@[simp]
abbrev Sorted : List α → Prop
  | [] | [_] => True
  | x :: x' :: xs => x ≤ x' ∧ Sorted (x' :: xs)

theorem sortExists (xs : List α) : ∃ ys, Sorted ys ∧ xs.Perm ys :=
  ⟨xs, by
    induction xs
    case nil => simp
    case cons _ xs _ => induction xs <;> simp; grind⟩