proposition: Lemma quick_sorted_aux3 : forall l e, let (l1,_) := partition e l in forall a, mem EDS.eq_A a l1 -> o a e.
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 _H]. contradiction. intros a [a_eq_a' | a_in_l1']; [idtac | rewrite H in IH; apply IH; trivial]. generalize (o_bool_ok a' e); dummy a a' a_eq_a'; subst; rewrite a'_lt_e; trivial. intros; rewrite H in IH; apply IH; trivial. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)