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: Hask.Ltac Hask.Control.Monad Hask.Data.Eq Hask.Data.Maybe Coq.Program.Wf Coq.Sorting.Sorted Coq.Classes.RelationClasses Coq.Lists.List FunctionalExtensionality Coq.Relations.Relations Coq.Reals.ROrderedType Coq.Lists.List Coq.Sorting.Sorted Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.RelationClasses FunctionalExtensionality