proposition: Lemma quick_sorted_aux1 : forall l1 l2 e, is_sorted l1 -> is_sorted l2 -> (forall a, mem EDS.eq_A a l1 -> o a e) -> (forall a, mem EDS.eq_A a l2 -> o e a) -> is_sorted (l1 ++ e :: l2).
proof: Proof. induction l1 as [ | e1 l1 ]; intros l2 e S1 S2 L1 L2. simpl; destruct l2 as [ | e2 l2]; intros; [apply is_sorted_cons1 | apply is_sorted_cons2 ]; trivial; apply (L2 e2); simpl; left; reflexivity. destruct l1 as [ | e1' l1] ; simpl; intros; apply is_sorted_cons2. apply L1; left; reflexivity. simpl in IHl1; apply IHl1; trivial; contradiction. inversion S1; trivial. rewrite app_comm_cons; apply IHl1; trivial. inversion S1; trivial. intros; apply L1; trivial; right; trivial. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)