proposition: Lemma Permutation_insert : forall A (a : A) R xs ys, Permutation xs ys -> Permutation (insert R a xs) (a :: ys).
proof: Proof. intros. rewrite H; clear H. induction ys; intros; simpl. constructor; trivial. unfold insert. destruct (R a0 a) eqn:Heqe; fold@insert. rewrite perm_swap. constructor. exact IHys. reflexivity. 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