fact: Fixpoint insert {a} (P : a -> a -> bool) (z : a) (l : list a) : list a := match l with | x :: xs => if P x z then x :: insert P z xs else z :: x :: xs | _ => [z] 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