fact: Fixpoint sortBy {a} (p : a -> a -> bool) (l : list a) : list a := match l with | [] => nil | x :: xs => insert p x (sortBy p xs) end.
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