proposition: Lemma sorted_cons_min : forall l e, is_sorted (e :: l) -> (forall e', mem EDS.eq_A e' (e :: l) -> o e e').
proof: Proof. simpl; intros l e S e' [e'_eq_e | e'_in_l]. dummy e' e e'_eq_e; subst; trivial. generalize o_proof; intro O; inversion O as [R _ _]; apply R. generalize e S e' e'_in_l; clear e S e' e'_in_l; induction l as [ | a l ]. intros e _ e' e'_in_nil; elim e'_in_nil. simpl; intros e S e' [e'_eq_a | e'_in_l]. dummy e' a e'_eq_a; subst e'; inversion S; trivial. generalize o_proof; intro O; inversion O as [ _ T _ ]; apply T with a. inversion S; trivial. apply IHl; trivial; inversion S; trivial. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)