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: Coq.Lists.List Equations(Equations) Equations.Type.EqDec Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Maybe Coq.Lists.List Coq.Relations.Relations Coq.Reals.ROrderedType Coq.Lists.List