suppression de FSets (redevient une contrib)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4205 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 651 deletions

diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
deleted file mode 100644
index 70d9ff962..000000000
--- a/theories/FSets/FSetInterface.v
+++ /dev/null
@@ -1,651 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-(** Set interfaces *)
-
-Require Export Bool.
-Require Export PolyList.
-Require Export Sorting.
-Require Export Setoid.
-Set Implicit Arguments.
-
-(** Misc properties used in specifications. *)
-
-Section Misc.
-Variable A,B : Set.
-Variable eqA : A -> A -> Prop. 
-Variable eqB : B -> B -> Prop.
-
-(** Compatibility of a  boolean function with respect to an equality. *)
-Definition compat_bool := [f:A->bool] (x,y:A)(eqA x y) -> (f x)=(f y).
-
-(** Compatibility of a predicate with respect to an equality. *)
-Definition compat_P := [P:A->Prop](x,y:A)(eqA x y) -> (P x) -> (P y).
-
-(** Being in a list modulo an equality relation. *)
-Inductive InList [x:A] : (list A) -> Prop :=
-  | InList_cons_hd : (y:A)(l:(list A))(eqA x y) -> (InList x (cons y l))
-  | InList_cons_tl : (y:A)(l:(list A))(InList x l) -> (InList x (cons y l)).
-
-(** A list without redondancy. *)
-Inductive Unique : (list A) -> Prop := 
-  | Unique_nil : (Unique (nil A)) 
-  | Unique_cons : (x:A)(l:(list A)) ~(InList x l) -> (Unique l) -> (Unique (cons x l)).
-
-End Misc.
-
-Hint InList := Constructors InList.
-Hint InList := Constructors Unique.
-Hint sort := Constructors sort.
-Hint lelistA := Constructors lelistA.
-Hints Unfold compat_bool compat_P.
-
-(** * Ordered types *)
-
-Inductive Compare [X:Set; lt,eq:X->X->Prop; x,y:X] : Set :=
-  | Lt : (lt x y) -> (Compare lt eq x y)
-  | Eq : (eq x y) -> (Compare lt eq x y)
-  | Gt : (lt y x) -> (Compare lt eq x y).
-
-Module Type OrderedType.
-
-  Parameter t : Set.
-
-  Parameter eq : t -> t -> Prop.
-  Parameter lt : t -> t -> Prop.
-
-  Axiom eq_refl : (x:t) (eq x x).
-  Axiom eq_sym : (x,y:t) (eq x y) -> (eq y x).
-  Axiom eq_trans : (x,y,z:t) (eq x y) -> (eq y z) -> (eq x z).
- 
-  Axiom lt_trans : (x,y,z:t) (lt x y) -> (lt y z) -> (lt x z).
-  Axiom lt_not_eq : (x,y:t) (lt x y) -> ~(eq x y).
-
-  Parameter compare : (x,y:t)(Compare lt eq x y).
-
-  Hints Immediate eq_sym.
-  Hints Resolve eq_refl eq_trans lt_not_eq lt_trans.
-
-End OrderedType.
-
-(** * Non-dependent signature
-
-    Signature [S] presents sets as purely informative programs 
-    together with axioms *)
-
-Module Type S.
-
-  Declare Module E : OrderedType.
-  Definition elt := E.t.
-
-  Parameter t : Set. (** the abstract type of sets *)
- 
-  Parameter empty: t.
-  (** The empty set. *)
-
-  Parameter is_empty: t -> bool.
-  (** Test whether a set is empty or not. *)
-
-  Parameter mem: elt -> t -> bool.
-  (** [mem x s] tests whether [x] belongs to the set [s]. *)
-
-  Parameter add: elt -> t -> t.
-  (** [add x s] returns a set containing all elements of [s],
-  plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
-
-  Parameter singleton: elt -> t.
-  (** [singleton x] returns the one-element set containing only [x]. *)
-
-  Parameter remove: elt -> t -> t.
-  (** [remove x s] returns a set containing all elements of [s],
-  except [x]. If [x] was not in [s], [s] is returned unchanged. *)
-
-  Parameter union: t -> t -> t.
-  (** Set union. *)
-
-  Parameter inter: t -> t -> t.
-  (** Set intersection. *)
-
-  Parameter diff:  t -> t -> t.
-  (** Set difference. *)
-
-  Parameter eq : t -> t -> Prop.
-  Parameter lt : t -> t -> Prop.
-  Parameter compare: (s,s':t)(Compare lt eq s s').
-  (** Total ordering between sets. Can be used as the ordering function
-  for doing sets of sets. *)
-
-  Parameter equal:  t -> t -> bool.
-  (** [equal s1 s2] tests whether the sets [s1] and [s2] are
-  equal, that is, contain equal elements. *)
-
-  Parameter subset:  t -> t -> bool.
-  (** [subset s1 s2] tests whether the set [s1] is a subset of
-  the set [s2]. *)
-
-  (** Coq comment: [iter] is useless in a purely functional world *)
-  (**  iter: (elt -> unit) -> set -> unit. i*)
-  (** [iter f s] applies [f] in turn to all elements of [s].
-  The order in which the elements of [s] are presented to [f]
-  is unspecified. *)
-
-  Parameter fold:  (A:Set)(elt -> A -> A) -> t -> A -> A.
-  (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
-  where [x1 ... xN] are the elements of [s].
-  The order in which elements of [s] are presented to [f] is
-  unspecified. *)
-
-  Parameter for_all:  (elt -> bool) -> t -> bool.
-  (** [for_all p s] checks if all elements of the set
-  satisfy the predicate [p]. *)
-
-  Parameter exists:  (elt -> bool) -> t -> bool.
-  (** [exists p s] checks if at least one element of
-  the set satisfies the predicate [p]. *)
-
-  Parameter filter:  (elt -> bool) -> t -> t.
-  (** [filter p s] returns the set of all elements in [s]
-  that satisfy predicate [p]. *)
-
-  Parameter partition:  (elt -> bool) -> t -> t * t.
-  (** [partition p s] returns a pair of sets [(s1, s2)], where
-  [s1] is the set of all the elements of [s] that satisfy the
-  predicate [p], and [s2] is the set of all the elements of
-  [s] that do not satisfy [p]. *)
-
-  Parameter cardinal: t -> nat.
-  (** Return the number of elements of a set. *)
-  (** Coq comment: nat instead of int ... *)
-
-  Parameter elements: t -> (list elt).
-  (** Return the list of all elements of the given set.
-  The returned list is sorted in increasing order with respect
-  to the ordering [Ord.compare], where [Ord] is the argument
-  given to {!Set.Make}. *)
-
-  Parameter min_elt: t -> (option elt).
-  (** Return the smallest element of the given set
-  (with respect to the [Ord.compare] ordering), or raise
-  [Not_found] if the set is empty. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
-
-  Parameter max_elt: t -> (option elt).
-  (** Same as {!Set.S.min_elt}, but returns the largest element of the
-  given set. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
-
-  Parameter choose: t -> (option elt).
-  (** Return one element of the given set, or raise [Not_found] if
-  the set is empty. Which element is chosen is unspecified,
-  but equal elements will be chosen for equal sets. *)
-  (** Coq comment: [Not_found] is represented by the option type *)
-  (** Coq comment: We do not necessary choose equal elements from 
-     equal sets. *)
-
-  Section Spec. 
-
-  Variable s,s',s'' : t.
-  Variable x,y,z : elt.
-
-  Parameter In : elt -> t -> Prop.
-  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
-  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
-  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
-  Definition Empty := [s](a:elt)~(In a s).
-  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
-  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
-
-  (** Specification of [In] *)
-  Parameter In_1: (E.eq x y) -> (In x s) -> (In y s).
-
-  (** Specification of [eq] *)
-  Parameter eq_refl: (eq s s). 
-  Parameter eq_sym: (eq s s') -> (eq s' s).
-  Parameter eq_trans: (eq s s') -> (eq s' s'') -> (eq s s'').
- 
-  (** Specification of [lt] *)
-  Parameter lt_trans : (lt s s') -> (lt s' s'') -> (lt s s'').
-  Parameter lt_not_eq : (lt s s') -> ~(eq s s').
-
-  (** Specification of [mem] *)
-  Parameter mem_1: (In x s) -> (mem x s)=true.
-  Parameter mem_2: (mem x s)=true -> (In x s). 
- 
-  (** Specification of [equal] *) 
-  Parameter equal_1: (Equal s s') -> (equal s s')=true.
-  Parameter equal_2: (equal s s')=true -> (Equal s s').
-
-  (** Specification of [subset] *)
-  Parameter subset_1: (Subset s s') -> (subset s s')=true.
-  Parameter subset_2: (subset s s')=true -> (Subset s s').
-
-  (** Specification of [empty] *)
-  Parameter empty_1: (Empty empty).
-
-  (** Specification of [is_empty] *)
-  Parameter is_empty_1: (Empty s) -> (is_empty s)=true. 
-  Parameter is_empty_2: (is_empty s)=true -> (Empty s).
- 
-  (** Specification of [add] *)
-  Parameter add_1: (In x (add x s)).
-  Parameter add_2: (In y s) -> (In y (add x s)).
-  Parameter add_3: ~(E.eq x y) -> (In y (add x s)) -> (In y s). 
-
-  (** Specification of [remove] *)
-  Parameter remove_1: ~(In x (remove x s)).
-  Parameter remove_2: ~(E.eq x y) -> (In y s) -> (In y (remove x s)).
-  Parameter remove_3: (In y (remove x s)) -> (In y s).
-
-  (** Specification of [singleton] *)
-  Parameter singleton_1: (In y (singleton x)) -> (E.eq x y). 
-  Parameter singleton_2: (E.eq x y) -> (In y (singleton x)). 
-
-  (** Specification of [union] *)
-  Parameter union_1: (In x (union s s')) -> (In x s)\/(In x s').
-  Parameter union_2: (In x s) -> (In x (union s s')). 
-  Parameter union_3: (In x s') ->  (In x (union s s')).
-
-  (** Specification of [inter] *)
-  Parameter inter_1: (In x (inter s s')) -> (In x s).
-  Parameter inter_2: (In x (inter s s')) -> (In x s').
-  Parameter inter_3: (In x s) -> (In x s') ->  (In x (inter s s')).
-
-  (** Specification of [diff] *)
-  Parameter diff_1: (In x (diff s s')) -> (In x s). 
-  Parameter diff_2: (In x (diff s s')) -> ~(In x s').
-  Parameter diff_3: (In x s) -> ~(In x s') -> (In x (diff s s')).
- 
-  (** Specification of [fold] *)  
-  Parameter fold_1: 
-   (A:Set)(i:A)(f:elt->A->A)
-   (EX l:(list elt) | 
-       (Unique E.eq l) /\ 
-       ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-       (fold f s i)=(fold_right f i l)).
-
-  (** Specification of [cardinal] *)  
-  Parameter cardinal_1: 
-    (EX l:(list elt) | 
-        (Unique E.eq l) /\
-        ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-        (cardinal s)=(length l)).
-
-  Section Filter.
-  
-  Variable f:elt->bool.
-
-  (** Specification of [filter] *)
-  Parameter filter_1: (compat_bool E.eq f) -> (In x (filter f s)) -> (In x s). 
-  Parameter filter_2: (compat_bool E.eq f) -> (In x (filter f s)) -> (f x)=true. 
-  Parameter filter_3: 
-    (compat_bool E.eq f) -> (In x s) -> (f x)=true -> (In x (filter f s)).
-
-  (** Specification of [for_all] *)
-  Parameter for_all_1: 
-    (compat_bool E.eq f) -> (For_all [x](f x)=true s) -> (for_all f s)=true.
-  Parameter for_all_2: 
-    (compat_bool E.eq f) -> (for_all f s)=true -> (For_all [x](f x)=true s).
-
-  (** Specification of [exists] *)
-  Parameter exists_1: 
-    (compat_bool E.eq f) -> (Exists [x](f x)=true s) -> (exists f s)=true.
-  Parameter exists_2: 
-    (compat_bool E.eq f) -> (exists f s)=true -> (Exists [x](f x)=true s).
-
-  (** Specification of [partition] *)
-  Parameter partition_1: 
-    (compat_bool E.eq f) -> (Equal (fst ? ? (partition f s)) (filter f s)).
-  Parameter partition_2: 
-    (compat_bool E.eq f) -> 
-    (Equal (snd ? ? (partition f s)) (filter [x](negb (f x)) s)).
-
-  (** Specification of [elements] *)
-  Parameter elements_1: (In x s) -> (InList E.eq x (elements s)).
-  Parameter elements_2: (InList E.eq x (elements s)) -> (In x s).
-  Parameter elements_3: (sort E.lt (elements s)).  
-
-  (** Specification of [min_elt] *)
-  Parameter min_elt_1: (min_elt s) = (Some ? x) -> (In x s). 
-  Parameter min_elt_2: (min_elt s) = (Some ? x) -> (In y s) -> ~(E.lt y x). 
-  Parameter min_elt_3: (min_elt s) = (None ?) -> (Empty s).
-
-  (** Specification of [max_elt] *)  
-  Parameter max_elt_1: (max_elt s) = (Some ? x) -> (In x s). 
-  Parameter max_elt_2: (max_elt s) = (Some ? x) -> (In y s) -> ~(E.lt x y). 
-  Parameter max_elt_3: (max_elt s) = (None ?) -> (Empty s).
-
-  (** Specification of [choose] *)
-  Parameter choose_1: (choose s)=(Some ? x) -> (In x s).
-  Parameter choose_2: (choose s)=(None ?) -> (Empty s).
-  (*i Parameter choose_equal: 
-      (equal s s')=true -> (compare (choose s) (choose s'))=E. i*)
-
-  End Filter.
-  End Spec.
-
-  Notation "∅" := empty.
-  Notation "a ⋃ b" := (union a b) (at level 1).
-  Notation "a ⋂ b" := (inter a b) (at level 1). 
-  Notation "∥ a ∥" := (cardinal a) (at level 1).
-  Notation "a ∈ b" := (In a b) (at level 1).
-  Notation "a ∉ b" := ~(In a b) (at level 1).
-  Notation "a ≡ b" := (Equal a b) (at level 1).
-  Notation "a ≢ b" := ~(Equal a b) (at level 1).
-  Notation "a ⊆ b" := (Subset a b) (at level 1).
-  Notation "a ⊈ b" := ~(Subset a b) (at level 1).  
-
-  Hints Immediate 
-  In_1.
-  
-  Hints Resolve 
-  mem_1 mem_2
-  equal_1 equal_2
-  subset_1 subset_2
-  empty_1
-  is_empty_1 is_empty_2
-  choose_1
-  choose_2
-  add_1 add_2 add_3
-  remove_1 remove_2 remove_3
-  singleton_1 singleton_2
-  union_1 union_2 union_3
-  inter_1 inter_2 inter_3 
-  diff_1 diff_2 diff_3
-  filter_1 filter_2 filter_3
-  for_all_1 for_all_2
-  exists_1 exists_2
-  partition_1 partition_2
-  elements_1 elements_2 elements_3
-  min_elt_1 min_elt_2 min_elt_3
-  max_elt_1 max_elt_2 max_elt_3.
-
-End S.
-
-(** * Dependent signature 
-
-    Signature [Sdep] presents sets using dependent types *)
-
-Module Type Sdep.
-
-  Declare Module E : OrderedType.
-  Definition elt := E.t.
-
-  Parameter t : Set.
-
-  Parameter eq : t -> t -> Prop.
-  Parameter lt : t -> t -> Prop.
-  Parameter compare: (s,s':t)(Compare lt eq s s').
-
-  Parameter eq_refl: (s:t)(eq s s). 
-  Parameter eq_sym: (s,s':t)(eq s s') -> (eq s' s).
-  Parameter eq_trans: (s,s',s'':t)(eq s s') -> (eq s' s'') -> (eq s s'').
-  Parameter lt_trans : (s,s',s'':t)(lt s s') -> (lt s' s'') -> (lt s s'').
-  Parameter lt_not_eq : (s,s':t)(lt s s') -> ~(eq s s').
-
-  Parameter In : elt -> t -> Prop.
-  Definition Equal := [s,s'](a:elt)(In a s)<->(In a s').
-  Definition Subset := [s,s'](a:elt)(In a s)->(In a s').
-  Definition Add := [x:elt;s,s':t](y:elt)(In y s') <-> ((E.eq y x)\/(In y s)).
-  Definition Empty := [s](a:elt)~(In a s).
-  Definition For_all := [P:elt->Prop; s:t](x:elt)(In x s)->(P x).
-  Definition Exists := [P:elt->Prop; s:t](EX x:elt | (In x s)/\(P x)).
-
-  Parameter eq_In: (s:t)(x,y:elt)(E.eq x y) -> (In x s) -> (In y s).
-
-  Parameter empty : { s:t | Empty s }.
-
-  Parameter is_empty : (s:t){ Empty s }+{ ~(Empty s) }.
-
-  Parameter mem : (x:elt) (s:t) { (In x s) } + { ~(In x s) }.
-
-  Parameter add : (x:elt) (s:t) { s':t | (Add x s s') }.
-
-  Parameter singleton : (x:elt){ s:t | (y:elt)(In y s) <-> (E.eq x y)}.
-  
-  Parameter remove : (x:elt)(s:t)
-                     { s':t | (y:elt)(In y s') <-> (~(E.eq y x) /\ (In y s))}.
-
-  Parameter union : (s,s':t)
-                    { s'':t | (x:elt)(In x s'') <-> ((In x s)\/(In x s'))}.
-
-  Parameter inter : (s,s':t)
-                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\(In x s'))}.
-
-  Parameter diff : (s,s':t)
-                    { s'':t | (x:elt)(In x s'') <-> ((In x s)/\~(In x s'))}.
-
-  Parameter equal : (s,s':t){ Equal s s' } + { ~(Equal s s') }.
- 
-  Parameter subset : (s,s':t) { Subset s s' } + { ~(Subset s s') }.
-
-  Parameter fold : 
-   (A:Set)(f:elt->A->A)(s:t)(i:A) 
-   { r : A | (EX l:(list elt) | 
-                  (Unique E.eq l) /\
-                  ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-                  r = (fold_right f i l)) }.
-
-  Parameter cardinal : 
-    (s:t) { r : nat | (EX l:(list elt) | 
-                              (Unique E.eq l) /\ 
-                              ((x:elt)(In x s)<->(InList E.eq x l)) /\ 
-                              r = (length l)) }.
-
-  Parameter filter : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
-     { s':t | (compat_P E.eq P) -> (x:elt)(In x s') <-> ((In x s)/\(P x)) }.
-
-  Parameter for_all : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
-     { (compat_P E.eq P) -> (For_all P s) } + 
-     { (compat_P E.eq P) -> ~(For_all P s) }.
-  
-  Parameter exists : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
-     { (compat_P E.eq P) -> (Exists P s) } + 
-     { (compat_P E.eq P) -> ~(Exists P s) }.
-
-  Parameter partition : (P:elt->Prop)(Pdec:(x:elt){P x}+{~(P x)})(s:t)
-     { partition : t*t | 
-        let (s1,s2) = partition in 
-	(compat_P E.eq P) -> 
-	((For_all P s1) /\ 
-	 (For_all ([x]~(P x)) s2) /\
-	 (x:elt)(In x s)<->((In x s1)\/(In x s2))) }.
-
-  Parameter elements : 
-     (s:t){ l:(list elt) | (sort E.lt l) /\ (x:elt)(In x s)<->(InList E.eq x l)}.
-
-  Parameter min_elt : 
-     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt y x) s) } + { Empty s }.
-
-  Parameter max_elt : 
-     (s:t){ x:elt | (In x s) /\ (For_all [y]~(E.lt x y) s) } + { Empty s }.
-
-  Parameter choose : (s:t) { x:elt | (In x s)} + { Empty s }.
-
-  Notation "∅" := empty.
-  Notation "a ⋃ b" := (union a b) (at level 1).
-  Notation "a ⋂ b" := (inter a b) (at level 1).
-  Notation "a ∈ b" := (In a b) (at level 1).
-  Notation "a ∉ b" := ~(In a b) (at level 1).
-  Notation "a ≡ b" := (Equal a b) (at level 1).
-  Notation "a ≢ b" := ~(Equal a b) (at level 1).
-  Notation "a ⊆ b" := (Subset a b) (at level 1).
-  Notation "a ⊈ b" := ~(Subset a b) (at level 1).  
-	
-End Sdep.
-
-(** * Ordered types properties *)
-
-(** Additional properties that can be derived from signature
-    [OrderedType]. *)
-
-Module MoreOrderedType [O:OrderedType]. 
-
-  Lemma gt_not_eq : (x,y:O.t)(O.lt y x) -> ~(O.eq x y).
-  Proof.
-   Intros; Intro; Absurd (O.eq y x); Auto.
-  Qed.	
- 
-  Lemma eq_not_lt : (x,y:O.t)(O.eq x y) -> ~(O.lt x y).
-  Proof. 
-   Intros; Intro; Absurd (O.eq x y); Auto.
-  Qed.
-
-  Hints Resolve gt_not_eq eq_not_lt.
-
-  Lemma eq_not_gt : (x,y:O.t)(O.eq x y) -> ~(O.lt y x).
-  Proof. 
-   Auto. 
-  Qed.
-  
-  Lemma lt_antirefl : (x:O.t)~(O.lt x x).
-  Proof.
-   Intros; Intro; Absurd (O.eq x x); Auto. 
-  Qed.
-
-  Lemma lt_not_gt : (x,y:O.t)(O.lt x y) -> ~(O.lt y x).
-  Proof. 
-   Intros; Intro; Absurd (O.eq x x); EAuto.
-  Qed.
-
-  Hints Resolve eq_not_gt lt_antirefl lt_not_gt.
-
-  Lemma lt_eq : (x,y,z:O.t)(O.lt x y) -> (O.eq y z) -> (O.lt x z).
-  Proof. 
-   Intros; Case (O.compare x z); Intros; Auto.
-   Absurd (O.eq x y); EAuto.
-   Absurd (O.eq z y); EAuto. 
-  Qed. 
- 
-  Lemma eq_lt : (x,y,z:O.t)(O.eq x y) -> (O.lt y z) -> (O.lt x z).    
-  Proof.
-    Intros; Case (O.compare x z); Intros; Auto.
-   Absurd (O.eq y z); EAuto.
-   Absurd (O.eq x y); EAuto. 
-  Qed. 
-
-  Hints Immediate eq_lt lt_eq.
-
-  Lemma elim_compare_eq: 
-   (x,y:O.t) (O.eq x y) -> 
-      (EX H : (O.eq x y) | (O.compare x y) = (Eq ? H)).
-  Proof. 
-   Intros; Case (O.compare x y); Intros H'.
-   Absurd (O.eq x y); Auto. 
-   Exists H'; Auto.   
-   Absurd (O.eq x y); Auto.
-  Qed.
-
-  Lemma elim_compare_lt: 
-   (x,y:O.t) (O.lt x y) -> 
-      (EX H : (O.lt x y) | (O.compare x y) = (Lt ? H)).
-  Proof. 
-   Intros; Case (O.compare x y); Intros H'.
-   Exists H'; Auto.   
-   Absurd (O.eq x y); Auto. 
-   Absurd (O.lt x x); EAuto.
-  Qed.
-
-  Lemma elim_compare_gt: 
-   (x,y:O.t) (O.lt y x) -> 
-      (EX H : (O.lt y x) | (O.compare x y) = (Gt ? H)).
-  Proof. 
-   Intros; Case (O.compare x y); Intros H'.
-   Absurd (O.lt x x); EAuto.
-   Absurd (O.eq x y); Auto.
-   Exists H'; Auto.   
-  Qed.
-
-  Tactic Definition Comp_eq x y := 
-    Elim (!elim_compare_eq x y); 
-    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto]. 
-
-  Tactic Definition Comp_lt x y := 
-    Elim (!elim_compare_lt x y); 
-    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto]. 
-
-  Tactic Definition Comp_gt x y := 
-    Elim (!elim_compare_gt x y); 
-    [Intros _1 _2; Rewrite _2; Clear _1 _2 | Auto].
-
-  Lemma eq_dec : (x,y:O.t){(O.eq x y)}+{~(O.eq x y)}.
-  Proof.
-   Intros; Elim (O.compare x y);[Right|Left|Right];Auto.
-  Qed.
- 
-  Lemma lt_dec : (x,y:O.t){(O.lt x y)}+{~(O.lt x y)}.
-  Proof.
-   Intros; Elim (O.compare x y);[Left|Right|Right];Auto.
-  Qed.
-
-  (** Results concerning lists modulo E.eq *)
-  
-  Notation "'Sort' l" := (sort O.lt l) (at level 10, l at level 8).
-  Notation "'Inf' x l" := (lelistA O.lt x l) (at level 10, x,l at level 8).
-  Notation "'In' x l" := (InList O.eq x l) (at level 10, x,l at level 8).
-
-  Lemma In_eq: (s:(list O.t))(x,y:O.t)(O.eq x y) -> (In x s) -> (In y s).
-  Proof. 
-   Intros; Elim H0; Intuition; EAuto.
-  Qed.
-  Hints Immediate In_eq.
-  
-  Lemma Inf_lt : (s:(list O.t))(x,y:O.t)(O.lt x y) -> (Inf y s) -> (Inf x s).
-  Proof.
-  Intro s; Case s; Constructor; Inversion H0; EAuto.
-  Qed.
- 
-  Lemma Inf_eq : (s:(list O.t))(x,y:O.t)(O.eq x y) -> (Inf y s) -> (Inf x s).
-  Proof.
-  Intro s; Case s; Constructor; Inversion H0; EApply eq_lt; EAuto.
-  Qed.
-  Hints Resolve Inf_lt Inf_eq. 
-
-  Lemma In_sort: (s:(list O.t))(x,a:O.t)(Inf a s) -> (In x s) -> (Sort s) -> (O.lt a x).
-  Proof. 
-  Induction s.
-  Intros; Inversion H0.
-  Intros.
-  Inversion_clear H0; Inversion_clear H2; Inversion_clear H1.
-  EApply lt_eq; EAuto.
-  EAuto.
-  Qed.
-  
-  Lemma Inf_In : (l:(list O.t))(x:O.t)
-    ((y:O.t)(PolyList.In y l) -> (O.lt x y)) -> (Inf x l).
-  Proof.
-    Induction l; Simpl; Intros; Constructor; Auto.
-  Save.
- 
-  Lemma Inf_In_2 : (l:(list O.t))(x:O.t)
-    ((y:O.t)(In y l) -> (O.lt x y)) -> (Inf x l).
-  Proof.
-    Induction l; Simpl; Intros; Constructor; Auto.
-  Save.
-  
-  Lemma In_InList : (l:(list O.t))(x:O.t)(PolyList.In x l) -> (In x l).
-  Proof.
-   Induction l; Simpl; Intuition.
-    Subst; Auto.  
-  Save.
-  Hints Resolve In_InList.
-
-  Lemma Sort_Unique : (l:(list O.t))(Sort l) -> (Unique O.eq l).
-  Proof.
-  Induction l; Auto.
-  Intros x l' H H0.
-  Inversion_clear H0.
-  Constructor; Auto.  
-  Intro.
-  Absurd (O.lt x x); Auto.
-  EApply In_sort; EAuto.
-  Qed.
-
-End MoreOrderedType.
-