fact: Fixpoint insert (z:Z) (l:list Z) : list Z := match l with | nil => z :: nil | cons a l' => match Z_le_gt_dec z a with | left _ => z :: a :: l' | right _ => a :: (insert z l') end end.
imports: List ZArith RelationClasses Morphisms Extraction