proposition: Lemma quick_sorted_aux4 : forall l e, let (_,l2) := partition e l in forall a, mem EDS.eq_A a l2 -> o e a.
proof: Proof. intros l e; functional induction (partition e l) as [|l a' l' l_eq_a'_l' IH l1' l2' H a'_lt_e |l a' l' l_eq_a'_l' IH l1' l2' H a'_ge_e]. contradiction. intros; rewrite H in IH; apply IH; trivial. intros a [a_eq_a' | a_in_l1']; [subst | rewrite H in IH; apply IH]; trivial. dummy a a' a_eq_a'; subst; trivial. generalize (o_bool_ok a' e); rewrite a'_ge_e; intro a'_ge_e'. destruct (o_total e a'); intros. assumption. absurd (DOS.o a' e); assumption. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)