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 xs; intros; simpl. - constructor; trivial. - unfold insert. destruct (R a0 a) eqn:Heqe; fold@insert. + rewrite perm_swap. constructor. exact IHxs. + reflexivity. Qed.
imports: Coq.Sorting.Sorted Coq.Sorting.Permutation Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.List Category.Theory.Coq.Maybe