proposition: Lemma Permutation_sortBy : forall A (a : A) (R : A → A → bool) xs, Permutation (sortBy R xs) xs.
proof: Proof. induction xs; intros; simpl. - constructor. - apply Permutation_insert. exact IHxs. Qed.
imports: Coq.Sorting.Sorted Coq.Sorting.Permutation Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.List Category.Theory.Coq.Maybe