OrderedType implementation for various numerical datatypes + min/max structures

 - A richer OrderedTypeFull interface : OrderedType + predicate "le"
 - Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
 - By the way: as suggested by S. Lescuyer, specification of compare is
   now inductive
 - GenericMinMax: axiomatisation + properties of min and max out of
    OrderedTypeFull structures.
 - MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
    with also some domain-specific results, and compatibility layer
    with already existing results.
 - Some ML code of plugins had to be adapted, otherwise wrong "eq",
   "lt" or simimlar constants were found by functions like coq_constant.
 - Beware of the aliasing problems: for instance eq:=@eq t instead of
   eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
   instead of Z in statement of Zmax_spec).
 - Some Morphism declaration are now ambiguous: switch to new syntax
   anyway.
 - Misc adaptations of FSets/MSets
 - Classes/RelationPairs.v: from two relations over A and B, we
   inspect relations over A*B and their properties in terms of classes.

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

12 files changed, 1333 insertions, 879 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 5b0fb21ef..de7a20d4c 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -9,44 +9,19 @@
 (* $Id$ *)
 
 Require Export SetoidList.
+Require DecidableType2. (* No Import here, this is on purpose. *)
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Types with Equalities, and nothing more (for subtyping purpose) *)
-
-Module Type EqualityType.
-
-  Parameter Inline t : Type.
 
-  Parameter Inline eq : t -> t -> Prop.
-
-  Axiom eq_refl : forall x : t, eq x x.
-  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
-  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans.
+(** * Types with Equalities, and nothing more (for subtyping purpose) *)
 
-End EqualityType.
+Module Type EqualityType := DecidableType2.EqualityTypeOrig.
 
 (** * Types with decidable Equalities (but no ordering) *)
 
-Module Type DecidableType.
-
-  Parameter Inline t : Type.
-
-  Parameter Inline eq : t -> t -> Prop.
-
-  Axiom eq_refl : forall x : t, eq x x.
-  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
-  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-
-  Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
-
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans.
-
-End DecidableType.
+Module Type DecidableType := DecidableType2.DecidableTypeOrig.
 
 (** * Additional notions about keys and datas used in FMap *)
 
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index b1cd5bfa5..7b329dd5e 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -8,8 +8,7 @@
 
 (* $Id$ *)
 
-Require Export SetoidList.
-Require DecidableType. (* No Import here, this is on purpose *)
+Require Export RelationClasses.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -33,152 +32,88 @@ Module Type DecidableType.
   Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
 End DecidableType.
 
+(** * Old versions of [DecidableType], with reflexivity, symmetry,
+  transitivity as three separate axioms. *)
+
+Module Type EqualityTypeOrig.
+  Parameter Inline t : Type.
+  Parameter Inline eq : t -> t -> Prop.
+
+  Axiom eq_refl : forall x : t, eq x x.
+  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
+  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+
+  Hint Immediate eq_sym.
+  Hint Resolve eq_refl eq_trans.
+End EqualityTypeOrig.
+
+Module Type DecidableTypeOrig.
+  Include Type EqualityTypeOrig.
+  Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
+End DecidableTypeOrig.
+
 (** * Compatibility wrapper from/to the old version of [DecidableType] *)
 
-Module Type DecidableTypeOrig := DecidableType.DecidableType.
+(** Interestingly, a module can be at the same time a [DecidableType]
+    and a [DecidableTypeOrig]. For the sake of compatibility,
+    this will be the case of all [DecidableType] modules provided here.
+*)
 
-Module Backport_DT (E:DecidableType) <: DecidableTypeOrig.
+Module Backport_ET (E:EqualityType) <: EqualityTypeOrig.
  Include E.
  Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
  Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
  Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
-End Backport_DT.
+End Backport_ET.
 
-Module Update_DT (E:DecidableTypeOrig) <: DecidableType.
+Module Update_ET (E:EqualityTypeOrig) <: EqualityType.
  Include E.
  Instance eq_equiv : Equivalence eq.
  Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed.
+End Update_ET.
+
+Module Backport_DT (E:DecidableType) <: DecidableTypeOrig.
+ Include Backport_ET E.
+ Definition eq_dec := E.eq_dec.
+End Backport_DT.
+
+Module Update_DT (E:DecidableTypeOrig) <: DecidableType.
+ Include Update_ET E.
+ Definition eq_dec := E.eq_dec.
 End Update_DT.
 
+(** * UsualDecidableType
+
+   A particular case of [DecidableType] where the equality is
+   the usual one of Coq. *)
 
-(** * Additional notions about keys and datas used in FMap *)
-
-Module KeyDecidableType(D:DecidableType).
- Import D.
-
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
-
-  Definition eqk (p p':key*elt) := eq (fst p) (fst p').
-  Definition eqke (p p':key*elt) :=
-          eq (fst p) (fst p') /\ (snd p) = (snd p').
-
-  Hint Unfold eqk eqke.
-  Hint Extern 2 (eqke ?a ?b) => split.
-
-   (* eqke is stricter than eqk *)
-
-   Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
-   Proof.
-     unfold eqk, eqke; intuition.
-   Qed.
-
-  (* eqk, eqke are equalities *)
-
-  Instance eqk_equiv : Equivalence eqk.
-  Proof.
-   constructor; eauto.
-  Qed.
-
-  Instance eqke_equiv : Equivalence eqke.
-  Proof.
-   constructor. auto.
-   red; unfold eqke; intuition.
-   red; unfold eqke; intuition; [ eauto | congruence ].
-  Qed.
-
-  Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv).
-  Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv).
-
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke; induction 1; intuition.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
-
-  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
-  Proof.
-   intros. rewrite <- H; auto.
-  Qed.
-
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
-
-  Hint Unfold MapsTo In.
-
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
-
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y.
-  exists e; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
-
-  Global Instance MapsTo_compat :
-    Proper (eq==>Logic.eq==>Logic.eq==>iff) MapsTo.
-  Proof.
-  intros x x' Hxx' e e' Hee' l l' Hll'; subst.
-  unfold MapsTo.
-  assert (EQN : eqke (x,e') (x',e')) by (compute;auto).
-  rewrite EQN; intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof.
-  intros; rewrite <- H; auto.
-  Qed.
-
-  Global Instance In_compat : Proper (eq==>Logic.eq==>iff) In.
-  Proof.
-  intros x x' Hxx' l l' Hll'; subst l.
-  unfold In.
-  split; intros (e,He); exists e.
-  rewrite <- Hxx'; auto.
-  rewrite Hxx'; auto.
-  Qed.
-
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof.
-  intros; rewrite <- H; auto.
-  Qed.
-
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    inversion 1.
-    inversion_clear H0; eauto.
-    destruct H1; simpl in *; intuition.
-  Qed.
-
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   inversion_clear 1; compute in H0; intuition.
-  Qed.
-
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   inversion_clear 1; compute in H0; intuition.
-  Qed.
-
- End Elt.
-
- Hint Resolve In_inv_2 In_inv_3.
-
-End KeyDecidableType.
+Module Type UsualDecidableType.
+ Parameter Inline t : Type.
+ Definition eq := @eq t.
+ Program Instance eq_equiv : Equivalence eq.
+ Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
+End UsualDecidableType.
 
+(** a [UsualDecidableType] is in particular an [DecidableType]. *)
 
+Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
 
+(** an shortcut for easily building a UsualDecidableType *)
+
+Module Type MiniDecidableType.
+ Parameter Inline t : Type.
+ Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
+End MiniDecidableType.
+
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
+ Definition t:=M.t.
+ Definition eq := @eq M.t.
+ Program Instance eq_equiv : Equivalence eq.
+ Definition eq_dec := M.eq_dec.
+ (* For building DecidableTypeOrig at the same time: *)
+ Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
+End Make_UDT.
 
 
diff --git a/theories/Structures/DecidableType2Ex.v b/theories/Structures/DecidableType2Ex.v
index 7b9c052ec..2ce2b5662 100644
--- a/theories/Structures/DecidableType2Ex.v
+++ b/theories/Structures/DecidableType2Ex.v
@@ -8,61 +8,29 @@
 
 (* $Id$ *)
 
-Require Import DecidableType2.
+Require Import DecidableType2 Morphisms RelationPairs.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** * Examples of Decidable Type structures. *)
 
-(** A particular case of [DecidableType] where
-    the equality is the usual one of Coq. *)
-
-Module Type UsualDecidableType.
- Parameter Inline t : Type.
- Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
- Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
-End UsualDecidableType.
-
-(** a [UsualDecidableType] is in particular an [DecidableType]. *)
-
-Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
-
-(** an shortcut for easily building a UsualDecidableType *)
-
-Module Type MiniDecidableType.
- Parameter Inline t : Type.
- Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
-End MiniDecidableType.
-
-Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
- Definition t:=M.t.
- Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
- Definition eq_dec := M.eq_dec.
-End Make_UDT.
 
 (** From two decidable types, we can build a new DecidableType
    over their cartesian product. *)
 
 Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
 
- Definition t := prod D1.t D2.t.
+ Definition t := (D1.t * D2.t)%type.
 
- Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y).
+ Definition eq := (D1.eq * D2.eq)%signature.
 
  Instance eq_equiv : Equivalence eq.
- Proof.
- constructor.
- intros (x1,x2); red; simpl; auto.
- intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
- intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto.
- Qed.
 
  Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
  Proof.
  intros (x1,x2) (y1,y2); unfold eq; simpl.
- destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition.
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+  compute; intuition.
  Defined.
 
 End PairDecidableType.
@@ -70,7 +38,7 @@ End PairDecidableType.
 (** Similarly for pairs of UsualDecidableType *)
 
 Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
- Definition t := prod D1.t D2.t.
+ Definition t := (D1.t * D2.t)%type.
  Definition eq := @eq t.
  Program Instance eq_equiv : Equivalence eq.
  Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v
new file mode 100644
index 000000000..5a5caaab8
--- /dev/null
+++ b/theories/Structures/DecidableType2Facts.v
@@ -0,0 +1,141 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Import DecidableType2 SetoidList.
+
+
+(** * Keys and datas used in FMap *)
+
+Module KeyDecidableType(D:DecidableType).
+ Import D.
+
+ Section Elt.
+ Variable elt : Type.
+ Notation key:=t.
+
+  Definition eqk (p p':key*elt) := eq (fst p) (fst p').
+  Definition eqke (p p':key*elt) :=
+          eq (fst p) (fst p') /\ (snd p) = (snd p').
+
+  Hint Unfold eqk eqke.
+  Hint Extern 2 (eqke ?a ?b) => split.
+
+   (* eqke is stricter than eqk *)
+
+   Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
+   Proof.
+     unfold eqk, eqke; intuition.
+   Qed.
+
+  (* eqk, eqke are equalities *)
+
+  Instance eqk_equiv : Equivalence eqk.
+  Proof.
+   constructor; eauto.
+  Qed.
+
+  Instance eqke_equiv : Equivalence eqke.
+  Proof.
+   constructor. auto.
+   red; unfold eqke; intuition.
+   red; unfold eqke; intuition; [ eauto | congruence ].
+  Qed.
+
+  Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv).
+  Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv).
+
+  Lemma InA_eqke_eqk :
+     forall x m, InA eqke x m -> InA eqk x m.
+  Proof.
+    unfold eqke; induction 1; intuition.
+  Qed.
+  Hint Resolve InA_eqke_eqk.
+
+  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
+  Proof.
+   intros. rewrite <- H; auto.
+  Qed.
+
+  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
+  Definition In k m := exists e:elt, MapsTo k e m.
+
+  Hint Unfold MapsTo In.
+
+  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+
+  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
+  Proof.
+  firstorder.
+  exists x; auto.
+  induction H.
+  destruct y.
+  exists e; auto.
+  destruct IHInA as [e H0].
+  exists e; auto.
+  Qed.
+
+  Global Instance MapsTo_compat :
+    Proper (eq==>Logic.eq==>Logic.eq==>iff) MapsTo.
+  Proof.
+  intros x x' Hxx' e e' Hee' l l' Hll'; subst.
+  unfold MapsTo.
+  assert (EQN : eqke (x,e') (x',e')) by (compute;auto).
+  rewrite EQN; intuition.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof.
+  intros; rewrite <- H; auto.
+  Qed.
+
+  Global Instance In_compat : Proper (eq==>Logic.eq==>iff) In.
+  Proof.
+  intros x x' Hxx' l l' Hll'; subst l.
+  unfold In.
+  split; intros (e,He); exists e.
+  rewrite <- Hxx'; auto.
+  rewrite Hxx'; auto.
+  Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof.
+  intros; rewrite <- H; auto.
+  Qed.
+
+  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
+  Proof.
+    inversion 1.
+    inversion_clear H0; eauto.
+    destruct H1; simpl in *; intuition.
+  Qed.
+
+  Lemma In_inv_2 : forall k k' e e' l,
+      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
+  Proof.
+   inversion_clear 1; compute in H0; intuition.
+  Qed.
+
+  Lemma In_inv_3 : forall x x' l,
+      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+  Proof.
+   inversion_clear 1; compute in H0; intuition.
+  Qed.
+
+ End Elt.
+
+ Hint Resolve In_inv_2 In_inv_3.
+ (* TODO: (re-)populate with more hints after failed attempt of Global Hint *)
+
+End KeyDecidableType.
+
+
+
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
new file mode 100644
index 000000000..ed9c035a1
--- /dev/null
+++ b/theories/Structures/GenericMinMax.v
@@ -0,0 +1,507 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Import OrderedType2 OrderedType2Facts Setoid Morphisms Basics.
+
+(** * A Generic construction of min and max based on OrderedType *)
+
+(** ** First, an interface for types with [max] and/or [min] *)
+
+Module Type HasMax (Import O:OrderedTypeFull).
+ Parameter Inline max : t -> t -> t.
+ Parameter max_spec : forall x y,
+   (lt x y /\ eq (max x y) y)  \/  (le y x /\ eq (max x y) x).
+End HasMax.
+
+Module Type HasMin (Import O:OrderedTypeFull).
+ Parameter Inline min : t -> t -> t.
+ Parameter min_spec : forall x y,
+   (lt x y /\ eq (min x y) x)  \/  (le y x /\ eq (min x y) y).
+End HasMin.
+
+Module Type HasMinMax (Import O:OrderedTypeFull).
+ Include Type HasMax O.
+ Include Type HasMin O.
+End HasMinMax.
+
+
+(** ** Any [OrderedTypeFull] can be equipped by [max] and [min]
+    based on the compare function. *)
+
+Definition gmax {A} (cmp : A->A->comparison) x y :=
+ match cmp x y with Lt => y | _ => x end.
+Definition gmin {A} (cmp : A->A->comparison) x y :=
+ match cmp x y with Gt => y | _ => x end.
+
+Module GenericMinMax (Import O:OrderedTypeFull) <: HasMinMax O.
+
+ Definition max := gmax O.compare.
+ Definition min := gmin O.compare.
+
+ Lemma max_spec : forall x y,
+   (lt x y /\ eq (max x y) y)  \/  (le y x /\ eq (max x y) x).
+ Proof.
+  intros. rewrite le_lteq. unfold max, gmax.
+  destruct (compare_spec x y); auto.
+ Qed.
+
+ Lemma min_spec : forall x y,
+   (lt x y /\ eq (min x y) x)  \/  (le y x /\ eq (min x y) y).
+ Proof.
+  intros. rewrite le_lteq. unfold min, gmin.
+  destruct (compare_spec x y); auto.
+ Qed.
+
+End GenericMinMax.
+
+
+(** ** Consequences of the minimalist interface: facts about [max]. *)
+
+Module MaxProperties (Import O:OrderedTypeFull)(Import M:HasMax O).
+ Module Import OF := OrderedTypeFullFacts O.
+ Infix "<" := lt.
+ Infix "==" := eq (at level 70).
+ Infix "<=" := le.
+
+Instance max_compat : Proper (eq==>eq==>eq) max.
+Proof.
+intros x x' Hx y y' Hy.
+assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
+set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
+rewrite <- Hx, <- Hy in *.
+destruct (compare_spec x y); intuition; order.
+Qed.
+
+(** An alias to the [max_spec] of the interface. *)
+
+Lemma max_spec : forall n m,
+  (n < m /\ max n m == m)  \/ (m <= n /\ max n m == n).
+Proof. exact max_spec. Qed.
+
+(** A more symmetric version of [max_spec], based only on [le].
+    Beware that left and right alternatives overlap. *)
+
+Lemma max_spec_le : forall n m,
+ (n <= m /\ max n m == m) \/ (m <= n /\ max n m == n).
+Proof.
+ intros. destruct (max_spec n m); [left|right]; intuition; order.
+Qed.
+
+(** Another function satisfying the same specification is equal to [max]. *)
+
+Lemma max_unicity : forall n m p,
+ ((n < m /\ p == m)  \/ (m <= n /\ p == n)) ->  p == max n m.
+Proof.
+ intros. assert (Hm := max_spec n m).
+ destruct (compare_spec n m); intuition; order.
+Qed.
+
+Lemma max_unicity_ext : forall f,
+ (forall n m, (n < m /\ f n m == m)  \/ (m <= n /\ f n m == n)) ->
+ (forall n m, f n m == max n m).
+Proof.
+ intros. apply max_unicity; auto.
+Qed.
+
+(** Induction principles for [max]. *)
+
+Lemma max_case_strong : forall n m (P:t -> Type),
+  (forall x y, x==y -> P x -> P y) ->
+  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
+Proof.
+intros n m P Compat Hl Hr.
+assert (H:=compare_spec n m). assert (H':=max_spec n m).
+destruct (compare n m).
+apply (Compat m), Hr; inversion_clear H; intuition; order.
+apply (Compat m), Hr; inversion_clear H; intuition; order.
+apply (Compat n), Hl; inversion_clear H; intuition; order.
+Qed.
+
+Lemma max_case : forall n m (P:t -> Type),
+  (forall x y, x == y -> P x -> P y) ->
+  P n -> P m -> P (max n m).
+Proof.
+ intros. apply max_case_strong; auto.
+Defined.
+
+(** [max] returns one of its arguments. *)
+
+Lemma max_dec : forall n m, {max n m == n} + {max n m == m}.
+Proof.
+ intros n m. apply max_case; auto.
+ intros x y H [E|E]; [left|right]; order.
+Defined.
+
+(** [max] commutes with monotone functions. *)
+
+Lemma max_monotone: forall f,
+ (Proper (eq ==> eq) f) ->
+ (Proper (le ==> le) f) ->
+ forall x y, max (f x) (f y) == f (max x y).
+Proof.
+ intros f Eqf Lef x y.
+ destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (M.max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f x <= f y) by (apply Lef; order). order.
+ assert (f y <= f x) by (apply Lef; order). order.
+Qed.
+
+(** *** Semi-lattice algebraic properties of [max] *)
+
+Lemma max_id : forall n, max n n == n.
+Proof.
+ intros. destruct (M.max_spec n n); intuition.
+Qed.
+
+Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p.
+Proof.
+ intros.
+ destruct (M.max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
+ destruct (max_spec m p); intuition; order.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
+ destruct (max_spec m p); intuition; order.
+Qed.
+
+Lemma max_comm : forall n m, max n m == max m n.
+Proof.
+ intros.
+ destruct (M.max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq; auto.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
+ order.
+ destruct (M.max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; auto.
+ order.
+Qed.
+
+(** *** Least-upper bound properties of [max] *)
+
+Lemma max_l : forall n m, m <= n -> max n m == n.
+Proof.
+ intros. destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_r : forall n m, n <= m -> max n m == m.
+Proof.
+ intros. destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma le_max_l : forall n m, n <= max n m.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma le_max_r : forall n m, m <= max n m.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m.
+Proof.
+ intros n m p H; destruct (M.max_spec n m);
+  [right|left]; intuition; order.
+Qed.
+
+Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m.
+Proof.
+ intros. split. apply max_le.
+ destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m.
+Proof.
+ intros. destruct (M.max_spec n m); intuition;
+  order || (right; order) || (left; order).
+Qed.
+
+Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p.
+Proof.
+ intros; destruct (M.max_spec n m); intuition; order.
+Qed.
+
+Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m.
+Proof.
+ intros.
+ destruct (M.max_spec p n) as [(LT,E)|(LE,E)]; rewrite E.
+ assert (LE' := le_max_r p m). order.
+ apply le_max_l.
+Qed.
+
+Lemma max_le_compat_r : forall n m p, n <= m -> max n p <= max m p.
+Proof.
+ intros. rewrite (max_comm n p), (max_comm m p).
+ auto using max_le_compat_l.
+Qed.
+
+Lemma max_le_compat : forall n m p q, n <= m -> p <= q ->
+ max n p <= max m q.
+Proof.
+ intros  n m p q Hnm Hpq.
+ assert (LE := max_le_compat_l _ _ m Hpq).
+ assert (LE' := max_le_compat_r _ _ p Hnm).
+ order.
+Qed.
+
+End MaxProperties.
+
+
+(** ** Properties concernant [min], then both [min] and [max].
+
+   To avoid duplication of code, we exploit that [min] can be
+   seen as a [max] of the reversed order.
+*)
+
+Module MinMaxProperties (Import O:OrderedTypeFull)(Import M:HasMinMax O).
+ Include MaxProperties O M.
+
+ Module ORev := OrderedTypeRev O.
+ Module MRev <: HasMax ORev.
+  Definition max x y := M.min y x.
+  Definition max_spec x y := M.min_spec y x.
+ End MRev.
+ Module MPRev := MaxProperties ORev MRev.
+
+Instance min_compat : Proper (eq==>eq==>eq) min.
+Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed.
+
+Lemma min_spec : forall n m,
+ (n < m /\ min n m == n) \/ (m <= n /\ min n m == m).
+Proof. exact min_spec. Qed.
+
+Lemma min_spec_le : forall n m,
+ (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).
+Proof. intros. exact (MPRev.max_spec_le m n). Qed.
+
+Lemma min_case_strong : forall n m (P:O.t -> Type),
+ (forall x y, x == y -> P x -> P y) ->
+ (m<=n -> P m) -> (n<=m -> P n) -> P (min n m).
+Proof. intros. apply (MPRev.max_case_strong m n P); auto. Qed.
+
+Lemma min_case : forall n m (P:O.t -> Type),
+  (forall x y, x == y -> P x -> P y) ->
+  P n -> P m -> P (min n m).
+Proof. intros. apply min_case_strong; auto. Defined.
+
+Lemma min_dec : forall n m, {min n m == n} + {min n m == m}.
+Proof.
+ intros. destruct (MPRev.max_dec m n); [right|left]; assumption.
+Defined.
+
+Lemma min_monotone: forall f,
+ (Proper (eq ==> eq) f) ->
+ (Proper (le ==> le) f) ->
+ forall x y, min (f x) (f y) == f (min x y).
+Proof.
+ intros. apply MPRev.max_monotone; auto. compute in *; eauto.
+Qed.
+
+Lemma min_unicity : forall n m p,
+ ((n < m /\ p == n)  \/ (m <= n /\ p == m)) ->  p == min n m.
+Proof. intros n m p. apply MPRev.max_unicity. Qed.
+
+Lemma min_unicity_ext : forall f,
+ (forall n m, (n < m /\ f n m == n)  \/ (m <= n /\ f n m == m)) ->
+ (forall n m, f n m == min n m).
+Proof. intros f H n m. apply MPRev.max_unicity, H; auto. Qed.
+
+Lemma min_id : forall n, min n n == n.
+Proof. intros. exact (MPRev.max_id n). Qed.
+
+Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p.
+Proof. intros. symmetry; apply MPRev.max_assoc. Qed.
+
+Lemma min_comm : forall n m, min n m == min m n.
+Proof. intros. exact (MPRev.max_comm m n). Qed.
+
+Lemma min_l : forall n m, n <= m -> min n m == n.
+Proof. intros n m. exact (MPRev.max_r m n). Qed.
+
+Lemma min_r : forall n m, m <= n -> min n m == m.
+Proof. intros n m. exact (MPRev.max_l m n). Qed.
+
+Lemma le_min_r : forall n m, min n m <= m.
+Proof. intros. exact (MPRev.le_max_l m n). Qed.
+
+Lemma le_min_l : forall n m, min n m <= n.
+Proof. intros. exact (MPRev.le_max_r m n). Qed.
+
+Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p.
+Proof. intros n m p H. destruct (MPRev.max_le _ _ _ H); auto. Qed.
+
+Lemma min_le_iff : forall n m p, min n m <= p <-> n <= p \/ m <= p.
+Proof. intros n m p. rewrite (MPRev.max_le_iff m n p); intuition. Qed.
+
+Lemma min_lt_iff : forall n m p, min n m < p <-> n < p \/ m < p.
+Proof. intros n m p. rewrite (MPRev.max_lt_iff m n p); intuition. Qed.
+
+Lemma min_glb_l : forall n m p, p <= min n m -> p <= n.
+Proof. intros n m. exact (MPRev.max_lub_r m n). Qed.
+
+Lemma min_glb_r : forall n m p, p <= min n m -> p <= m.
+Proof. intros n m. exact (MPRev.max_lub_l m n). Qed.
+
+Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m.
+Proof. intros. apply MPRev.max_lub; auto. Qed.
+
+Lemma min_glb_iff : forall n m p, p <= min n m <-> p <= n /\ p <= m.
+Proof. intros. rewrite (MPRev.max_lub_iff m n p); intuition. Qed.
+
+Lemma min_glb_lt : forall n m p, p < n -> p < m -> p < min n m.
+Proof. intros. apply MPRev.max_lub_lt; auto. Qed.
+
+Lemma min_glb_lt_iff : forall n m p, p < min n m <-> p < n /\ p < m.
+Proof. intros. rewrite (MPRev.max_lub_lt_iff m n p); intuition. Qed.
+
+Lemma min_le_compat_l : forall n m p, n <= m -> min p n <= min p m.
+Proof. intros n m. exact (MPRev.max_le_compat_r m n). Qed.
+
+Lemma min_le_compat_r : forall n m p, n <= m -> min n p <= min m p.
+Proof. intros n m. exact (MPRev.max_le_compat_l m n). Qed.
+
+Lemma min_le_compat : forall n m p q, n <= m -> p <= q ->
+ min n p <= min m q.
+Proof. intros. apply MPRev.max_le_compat; auto. Qed.
+
+
+(** *** Combined properties of min and max *)
+
+Lemma min_max_absorption : forall n m, max n (min n m) == n.
+Proof.
+ intros.
+ destruct (M.min_spec n m) as [(C,E)|(C,E)]; rewrite E.
+ apply max_l. OF.order.
+ destruct (M.max_spec n m); intuition; OF.order.
+Qed.
+
+Lemma max_min_absorption : forall n m, min n (max n m) == n.
+Proof.
+ intros.
+ destruct (M.max_spec n m) as [(C,E)|(C,E)]; rewrite E.
+ destruct (M.min_spec n m) as [(C',E')|(C',E')]; auto. OF.order.
+ apply min_l; auto. OF.order.
+Qed.
+
+(** Distributivity *)
+
+Lemma max_min_distr : forall n m p,
+ max n (min m p) == min (max n m) (max n p).
+Proof.
+ intros. symmetry. apply min_monotone.
+ eauto with *.
+ repeat red; intros. apply max_le_compat_l; auto.
+Qed.
+
+Lemma min_max_distr : forall n m p,
+ min n (max m p) == max (min n m) (min n p).
+Proof.
+ intros. symmetry. apply max_monotone.
+ eauto with *.
+ repeat red; intros. apply min_le_compat_l; auto.
+Qed.
+
+(** Modularity *)
+
+Lemma max_min_modular : forall n m p,
+ max n (min m (max n p)) == min (max n m) (max n p).
+Proof.
+ intros. rewrite <- max_min_distr.
+ destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto.
+ destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'.
+ rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto.
+ rewrite 2 max_l; try OF.order. rewrite min_le_iff; auto.
+Qed.
+
+Lemma min_max_modular : forall n m p,
+ min n (max m (min n p)) == max (min n m) (min n p).
+Proof.
+ intros. rewrite <- min_max_distr.
+ destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto.
+ destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'.
+ rewrite 2 min_l; try OF.order. rewrite max_le_iff; right; OF.order.
+ rewrite 2 min_l; try OF.order. rewrite max_le_iff; auto.
+Qed.
+
+(** Disassociativity *)
+
+Lemma max_min_disassoc : forall n m p,
+ min n (max m p) <= max (min n m) p.
+Proof.
+ intros. rewrite min_max_distr.
+ auto using max_le_compat_l, le_min_r.
+Qed.
+
+(** Anti-monotonicity swaps the role of [min] and [max] *)
+
+Lemma max_min_antimonotone : forall f,
+ Proper (eq==>eq) f ->
+ Proper (le==>inverse le) f ->
+ forall x y, max (f x) (f y) == f (min x y).
+Proof.
+ intros f Eqf Lef x y.
+ destruct (M.min_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (M.max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f y <= f x) by (apply Lef; OF.order). OF.order.
+ assert (f x <= f y) by (apply Lef; OF.order). OF.order.
+Qed.
+
+
+Lemma min_max_antimonotone : forall f,
+ Proper (eq==>eq) f ->
+ Proper (le==>inverse le) f ->
+ forall x y, min (f x) (f y) == f (max x y).
+Proof.
+ intros f Eqf Lef x y.
+ destruct (M.max_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (M.min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f y <= f x) by (apply Lef; OF.order). OF.order.
+ assert (f x <= f y) by (apply Lef; OF.order). OF.order.
+Qed.
+
+End MinMaxProperties.
+
+
+
+(** Some Remaining questions...
+
+--> Compare with a type-classes version ?
+
+--> Is max_unicity and max_unicity_ext really convenient to express
+    that any possible definition of max will in fact be equivalent ?
+
+--> Is it possible to avoid copy-paste about min even more ?
+
+--> Can this modular approach be used for more complex things,
+    in particular div/mod ?
+    How can we share common parts between nat and Z in this case ?
+    How to handle different choices (Zdiv vs. ZOdiv) ?
+
+*)
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 31c9324f8..8a3635686 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -27,7 +27,7 @@ Set Implicit Arguments.
    a strict order [lt] total and compatible with [eq], and
    a larger order [le] synonym of [lt\/eq]. *)
 
-Module Type OrderTacSig.
+Module Type OrderSig.
 
 Parameter Inline t : Type.
 Parameters eq lt le : t -> t -> Prop.
@@ -37,7 +37,7 @@ Instance lt_compat : Proper (eq==>eq==>iff) lt.
 Parameter lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
 Parameter le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
 
-End OrderTacSig.
+End OrderSig.
 
 (** NB : we should _not_ use "Inline" for these predicates,
    otherwise the ltac matching will not work properly later. *)
@@ -60,7 +60,7 @@ Infix "+" := trans_ord : order.
 
 (** ** [MakeOrderTac] : The functor providing the order tactic. *)
 
-Module MakeOrderTac(Import O:OrderTacSig).
+Module MakeOrderTac(Import O:OrderSig).
 
 Local Open Scope order.
 
@@ -249,7 +249,8 @@ end.
 
 (** The complete tactic. *)
 
-Ltac order := intros; order_prepare; order_loop; fail.
+Ltac order :=
+ intros; order_prepare; order_loop; fail "Order tactic unsuccessful".
 
 End MakeOrderTac.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index a8e1ebdd6..f0d4163c3 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -103,7 +103,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
   Proof. intros; destruct (compare x y); auto. Qed.
 
-  Module OrderElts : OrderTacSig
+  Module OrderElts : OrderSig
     with Definition t := t
     with Definition eq := eq
     with Definition lt := lt.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 16da2162d..4d62c2716 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -8,18 +8,19 @@
 
 (* $Id$ *)
 
-Require Export SetoidList DecidableType2 OrderTac.
+Require Export Relations Morphisms Setoid DecidableType2.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** * Ordered types *)
 
-Definition Cmp (A:Type)(eq lt : relation A) c :=
- match c with
-  | Eq => eq
-  | Lt => lt
-  | Gt => flip lt
- end.
+Inductive Cmp {A} (eq lt:relation A)(x y : A) : comparison -> Prop :=
+| Cmp_eq : eq x y -> Cmp eq lt x y Eq
+| Cmp_lt : lt x y -> Cmp eq lt x y Lt
+| Cmp_gt : lt y x -> Cmp eq lt x y Gt.
+
+Hint Constructors Cmp.
+
 
 Module Type MiniOrderedType.
   Include Type EqualityType.
@@ -29,10 +30,11 @@ Module Type MiniOrderedType.
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
   Parameter compare : t -> t -> comparison.
-  Axiom compare_spec : forall x y, Cmp eq lt (compare x y) x y.
+  Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y).
 
 End MiniOrderedType.
 
+
 Module Type OrderedType.
   Include Type MiniOrderedType.
 
@@ -42,492 +44,60 @@ Module Type OrderedType.
 
 End OrderedType.
 
+
 Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType.
   Include O.
 
   Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
   Proof.
    intros.
-   generalize (compare_spec x y); destruct (compare x y);
-    unfold Cmp, flip; intros.
-    left; auto.
-    right. intro H'; rewrite <- H' in H.
-      apply (StrictOrder_Irreflexive x); auto.
-    right. intro H'; rewrite <- H' in H.
-      apply (StrictOrder_Irreflexive x); auto.
+   assert (H:=compare_spec x y); destruct (compare x y).
+   left; inversion_clear H; auto.
+   right; inversion_clear H. intro H'. rewrite H' in *.
+      apply (StrictOrder_Irreflexive y); auto.
+   right; inversion_clear H. intro H'. rewrite H' in *.
+      apply (StrictOrder_Irreflexive y); auto.
   Defined.
 
 End MOT_to_OT.
 
-(** * Ordered types properties *)
-
-(** Additional properties that can be derived from signature
-    [OrderedType]. *)
-
-Module OrderedTypeFacts (Import O: OrderedType).
-
-  Infix "==" := eq (at level 70, no associativity) : order.
-  Infix "<" := lt : order.
-  Notation "x <= y" := (~lt y x) : order.
-  Infix "?=" := compare (at level 70, no associativity) : order.
-
-  Local Open Scope order.
-
-  Ltac elim_compare x y :=
-   generalize (compare_spec x y); destruct (compare x y);
-   unfold Cmp, flip.
-
-  Module OrderElts : OrderTacSig
-    with Definition t := t
-    with Definition eq := eq
-    with Definition lt := lt.
-  (* Opaque signature is crucial for ltac to work correctly later *)
-  Include O.
-  Definition le x y := x<y \/ x==y.
-  Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
-  Proof. intros; elim_compare x y; intuition. Qed.
-  Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
-  Proof. unfold le; intuition. Qed.
-  End OrderElts.
-  Module OrderTac := MakeOrderTac OrderElts.
-
-  Ltac order :=
-    change eq with OrderElts.eq in *;
-    change lt with OrderElts.lt in *;
-    OrderTac.order.
-
-  (** The following lemmas are either re-phrasing of [eq_equiv] and
-      [lt_strorder] or immediately provable by [order]. Interest:
-      compatibility, test of order, etc *)
-
-  Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x.
-
-  Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y.
-
-  Definition eq_trans (x y z:t) : x==y -> y==z -> x==z :=
-   Equivalence_Transitive x y z.
-
-  Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
-   StrictOrder_Transitive x y z.
-
-  Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
-
-  (** Some more about [compare] *)
-
-  Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
-  Proof.
-   intros; elim_compare x y; intuition; try discriminate; order.
-  Qed.
-
-  Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y.
-  Proof.
-   intros; elim_compare x y; intuition; try discriminate; order.
-  Qed.
-
-  Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x.
-  Proof.
-   intros; elim_compare x y; intuition; try discriminate; order.
-  Qed.
-
-  Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x.
-  Proof.
-   intros; rewrite compare_lt_iff; intuition.
-  Qed.
-
-  Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y.
-  Proof.
-   intros; rewrite compare_gt_iff; intuition.
-  Qed.
-
-  Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
-
-  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
-  Proof.
-  intros x x' Hxx' y y' Hyy'.
-  elim_compare x' y'; intros; autorewrite with order; order.
-  Qed.
-
-  Lemma compare_refl : forall x, (x ?= x) = Eq.
-  Proof.
-   intros; elim_compare x x; auto; order.
-  Qed.
-
-  Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
-  Proof.
-   intros; elim_compare x y; simpl; intros; autorewrite with order; order.
-  Qed.
-
-  (** For compatibility reasons *)
-  Definition eq_dec := eq_dec.
-
-  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
-  Proof.
-   intros; elim_compare x y; [ right | left | right ]; order.
-  Defined.
-
-  Definition eqb x y : bool := if eq_dec x y then true else false.
-
-  Lemma if_eq_dec : forall x y (B:Type)(b b':B),
-    (if eq_dec x y then b else b') =
-    (match compare x y with Eq => b | _ => b' end).
-  Proof.
-  intros; destruct eq_dec; elim_compare x y; auto; order.
-  Qed.
-
-  Lemma eqb_alt :
-    forall x y, eqb x y = match compare x y with Eq => true | _ => false end.
-  Proof.
-  unfold eqb; intros; apply if_eq_dec.
-  Qed.
-
-  Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb.
-  Proof.
-  intros x x' Hxx' y y' Hyy'.
-  rewrite 2 eqb_alt, Hxx', Hyy'; auto.
-  Qed.
-
-
-(* Specialization of resuts about lists modulo. *)
-
-Section ForNotations.
-
-Notation In:=(InA eq).
-Notation Inf:=(lelistA lt).
-Notation Sort:=(sort lt).
-Notation NoDup:=(NoDupA eq).
-
-Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-Proof. intros. rewrite <- H; auto. Qed.
-
-Lemma ListIn_In : forall l x, List.In x l -> In x l.
-Proof. exact (In_InA eq_equiv). Qed.
-
-Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_ltA lt_strorder). Qed.
-
-Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
-
-Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
-Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
-
-Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
-Proof. exact (@In_InfA t lt). Qed.
-
-Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
-Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
-
-Lemma Inf_alt :
- forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
-Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
-
-Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
-Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed.
-
-End ForNotations.
-
-Hint Resolve ListIn_In Sort_NoDup Inf_lt.
-Hint Immediate In_eq Inf_lt.
-
-End OrderedTypeFacts.
-
-
-(** Some tests of [order] : is it at least capable of
-    proving some basic properties ? *)
 
-Module OrderedTypeTest (O:OrderedType).
-  Module Import MO := OrderedTypeFacts O.
-  Local Open Scope order.
-  Lemma lt_not_eq x y : x<y -> ~x==y.  Proof. order. Qed.
-  Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed.
-  Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed.
-  Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed.
-  Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed.
-  Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed.
-  Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed.
-  Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed.
-  Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed.
-  Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed.
-  Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed.
-  Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed.
-  Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed.
-  Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed.
-  Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed.
-  Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed.
-  Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed.
-  Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed.
-End OrderedTypeTest.
+(** * UsualOrderedType
 
+    A particular case of [OrderedType] where the equality is
+    the usual one of Coq. *)
 
-(** * Relations over pairs (TO MIGRATE in some TypeClasses file) *)
+Module Type UsualOrderedType.
+ Include Type UsualDecidableType.
 
-Definition ProdRel {A B}(RA:relation A)(RB:relation B) : relation (A*B) :=
- fun p p' => RA (fst p) (fst p') /\ RB (snd p) (snd p').
+ Parameter Inline lt : t -> t -> Prop.
+ Instance lt_strorder : StrictOrder lt.
+ (* The following is useless since eq is Leibniz, but should be there
+    for subtyping... *)
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
-Definition FstRel {A B}(R:relation A) : relation (A*B) :=
- fun p p' => R (fst p) (fst p').
+ Parameter compare : t -> t -> comparison.
+ Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y).
 
-Definition SndRel {A B}(R:relation B) : relation (A*B) :=
- fun p p' => R (snd p) (snd p').
+End UsualOrderedType.
 
-Generalizable Variables A B RA RB Ri Ro.
+(** a [UsualOrderedType] is in particular an [OrderedType]. *)
 
-Instance ProdRel_equiv {A B} `(Equivalence A RA)`(Equivalence B RB) :
- Equivalence (ProdRel RA RB).
-Proof. firstorder. Qed.
+Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U.
 
-Instance FstRel_equiv {A B} `(Equivalence A RA) :
- Equivalence (FstRel RA (B:=B)).
-Proof. firstorder. Qed.
 
-Instance SndRel_equiv {A B} `(Equivalence B RB) :
- Equivalence (SndRel RB (A:=A)).
-Proof. firstorder. Qed.
+(** * OrderedType with also a [<=] predicate *)
 
-Instance FstRel_strorder {A B} `(StrictOrder A RA) :
- StrictOrder (FstRel RA (B:=B)).
-Proof. firstorder. Qed.
+Module Type OrderedTypeFull.
+ Include Type OrderedType.
+ Parameter Inline le : t -> t -> Prop.
+ Axiom le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+End OrderedTypeFull.
 
-Instance SndRel_strorder {A B} `(StrictOrder B RB) :
- StrictOrder (SndRel RB (A:=A)).
-Proof. firstorder. Qed.
-
-Lemma FstRel_ProdRel {A B}(RA:relation A) : forall p p':A*B,
- (FstRel RA) p p' <-> (ProdRel RA (fun _ _ =>True)) p p'.
-Proof. firstorder. Qed.
-
-Lemma SndRel_ProdRel {A B}(RB:relation B) : forall p p':A*B,
- (SndRel RB) p p' <-> (ProdRel (fun _ _ =>True) RB) p p'.
-Proof. firstorder. Qed.
-
-Lemma ProdRel_alt {A B}(RA:relation A)(RB:relation B) : forall p p':A*B,
- (ProdRel RA RB) p p' <-> relation_conjunction (FstRel RA) (SndRel RB) p p'.
-Proof. firstorder. Qed.
-
-Instance FstRel_compat {A B} (R : relation A)`(Proper _ (Ri==>Ri==>Ro) R) :
- Proper (FstRel Ri==>FstRel Ri==>Ro) (FstRel R (B:=B)).
-Proof.
- intros A B R Ri Ro H (a1,b1) (a1',b1') Hab1 (a2,b2) (a2',b2') Hab2.
- unfold FstRel in *; simpl in *. apply H; auto.
-Qed.
-
-Instance SndRel_compat {A B} (R : relation B)`(Proper _ (Ri==>Ri==>Ro) R) :
- Proper (SndRel Ri==>SndRel Ri==>Ro) (SndRel R (A:=A)).
-Proof.
- intros A B R Ri Ro H (a1,b1) (a1',b1') Hab1 (a2,b2) (a2',b2') Hab2.
- unfold SndRel in *; simpl in *. apply H; auto.
-Qed.
-
-Instance FstRel_sub {A B} (RA:relation A)(RB:relation B):
- subrelation (ProdRel RA RB) (FstRel RA).
-Proof. firstorder. Qed.
-
-Instance SndRel_sub {A B} (RA:relation A)(RB:relation B):
- subrelation (ProdRel RA RB) (SndRel RB).
-Proof. firstorder. Qed.
-
-Instance pair_compat { A B } (RA:relation A)(RB : relation B) :
- Proper (RA==>RB==>ProdRel RA RB) (@pair A B).
-Proof. firstorder. Qed.
-
-
-Hint Unfold ProdRel FstRel SndRel.
-Hint Extern 2 (ProdRel _ _ _ _) => split.
-
-
-Module KeyOrderedType(Import O:OrderedType).
- Module Import MO:=OrderedTypeFacts(O).
-
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
-
-  Definition eqk : relation (key*elt) := FstRel eq.
-  Definition eqke : relation (key*elt) := ProdRel eq Logic.eq.
-  Definition ltk : relation (key*elt) := FstRel lt.
-
-  Hint Unfold eqk eqke ltk.
-
-  (* eqke is stricter than eqk *)
-
-  Global Instance eqke_eqk : subrelation eqke eqk.
-  Proof. unfold eqke, eqk; auto with *. Qed.
-
-  (* eqk, eqke are equalities, ltk is a strict order *)
-
-  Global Instance eqk_equiv : Equivalence eqk.
-
-  Global Instance eqke_equiv : Equivalence eqke.
-
-  Global Instance ltk_strorder : StrictOrder ltk.
-
-  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
-  Proof. unfold eqk, ltk; auto with *. Qed.
-
-  (* Additionnal facts *)
-
-  Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt).
-  Proof. unfold eqke; auto with *. Qed.
-
-  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
-  Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
-  elim (StrictOrder_Irreflexive _ LT).
-  Qed.
-
-  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
-  Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
-  elim (StrictOrder_Irreflexive _ LT).
-  Qed.
-
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke, ProdRel; induction 1; intuition.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
-
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
-  Notation Sort := (sort ltk).
-  Notation Inf := (lelistA ltk).
-
-  Hint Unfold MapsTo In.
-
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
-
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y; compute in H.
-  exists e; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
-
-  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
-  Proof.
-  unfold In, MapsTo.
-  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
-  firstorder.
-  exists (snd x), x; auto.
-  Qed.
-
-  Lemma In_nil : forall k, In k nil <-> False.
-  Proof.
-  intros; rewrite In_alt2; apply Exists_nil.
-  Qed.
-
-  Lemma In_cons : forall k p l,
-   In k (p::l) <-> eq k (fst p) \/ In k l.
-  Proof.
-  intros; rewrite !In_alt2, Exists_cons; intuition.
-  Qed.
-
-  Global Instance MapsTo_compat :
-   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
-  Proof.
-  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
-  rewrite Hx, He, Hl; intuition.
-  Qed.
-
-  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
-  Proof.
-  intros x x' Hx l l' Hl. rewrite !In_alt.
-  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. intros l x x' H. rewrite H; auto. Qed.
-
-  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
-  Proof. apply InfA_ltA; auto with *. Qed.
-
-  Hint Immediate Inf_eq.
-  Hint Resolve Inf_lt.
-
-  Lemma Sort_Inf_In :
-      forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
-  Proof. apply SortA_InfA_InA; auto with *. Qed.
-
-  Lemma Sort_Inf_NotIn :
-      forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
-  Proof.
-    intros; red; intros.
-    destruct H1 as [e' H2].
-    elim (@ltk_not_eqk (k,e) (k,e')).
-    eapply Sort_Inf_In; eauto.
-    red; simpl; auto.
-  Qed.
-
-  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
-  Proof. apply SortA_NoDupA; auto with *. Qed.
-
-  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
-  Proof.
-   intros; invlist sort; eapply Sort_Inf_In; eauto.
-  Qed.
-
-  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
-      ltk e e' \/ eqk e e'.
-  Proof.
-    intros; invlist InA; auto.
-    left; apply Sort_In_cons_1 with l; auto.
-  Qed.
-
-  Lemma Sort_In_cons_3 :
-    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
-  Proof.
-    intros; invlist sort; red; intros.
-    eapply Sort_Inf_NotIn; eauto using In_eq.
-  Qed.
-
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
-    right; exists x; auto.
-  Qed.
-
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   intros; invlist InA; intuition.
-  Qed.
-
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   intros; invlist InA; compute in * |- ; intuition.
-  Qed.
-
- End Elt.
-
- Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqk_equiv elt)).
- Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqk_equiv elt)).
- Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqk_equiv elt)).
- Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqke_equiv elt)).
- Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqke_equiv elt)).
- Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqke_equiv elt)).
- Hint Resolve (fun elt => @StrictOrder_Transitive _ _ (ltk_strorder elt)).
-
- Hint Unfold eqk eqke ltk.
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve ltk_not_eqk ltk_not_eqke.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
- Hint Immediate Inf_eq.
- Hint Resolve Inf_lt.
- Hint Resolve Sort_Inf_NotIn.
- Hint Resolve In_inv_2 In_inv_3.
-
-End KeyOrderedType.
+Module OT_to_Full (O:OrderedType) <: OrderedTypeFull.
+ Include O.
+ Definition le x y := lt x y \/ eq x y.
+ Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+ Proof. unfold le; split; auto. Qed.
+End OT_to_Full.
 
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v
index 6c2fb0d3f..4e14f5128 100644
--- a/theories/Structures/OrderedType2Alt.v
+++ b/theories/Structures/OrderedType2Alt.v
@@ -76,7 +76,7 @@ Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
     | GT _ => Gt
   end.
 
- Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y.
+ Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
  Proof.
   intros; unfold compare; destruct O.compare; auto.
  Qed.
@@ -101,8 +101,9 @@ Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.
 
  Definition compare : forall x y, Compare lt eq x y.
  Proof.
-  intros. generalize (O.compare_spec x y); unfold Cmp, flip.
-  destruct (O.compare x y); [apply EQ|apply LT|apply GT]; auto.
+  intros. assert (H:=O.compare_spec x y).
+  destruct (O.compare x y); [apply EQ|apply LT|apply GT];
+   inversion H; auto.
  Defined.
 
 End Backport_OT.
@@ -168,10 +169,11 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
 
  Definition compare := O.compare.
 
- Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y.
+ Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
  Proof.
-  unfold Cmp, flip, eq, lt, compare; intros.
+  unfold eq, lt, compare; intros.
   destruct (O.compare x y) as [ ]_eqn:H; auto.
+  apply Cmp_gt.
   rewrite compare_sym, H; auto.
  Qed.
 
@@ -196,8 +198,8 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
    forall x y, (y?=x) = CompOpp (x?=y).
  Proof.
  intros x y; unfold compare.
- generalize (compare_spec x y) (compare_spec y x); unfold Cmp, flip.
- destruct (O.compare x y); destruct (O.compare y x); intros U V; auto.
+ destruct (compare_spec x y) as [U|U|U];
+  destruct (compare_spec y x) as [V|V|V]; auto.
  rewrite U in V. elim (StrictOrder_Irreflexive y); auto.
  rewrite U in V. elim (StrictOrder_Irreflexive y); auto.
  rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
@@ -209,8 +211,8 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
  Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y.
  Proof.
  unfold compare.
- intros x y; generalize (compare_spec x y).
- destruct (O.compare x y); intuition; try discriminate.
+ intros x y; destruct (compare_spec x y); intuition;
+  try discriminate.
  rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto.
  rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto.
  Qed.
@@ -218,8 +220,8 @@ Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
  Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y.
  Proof.
  unfold compare.
- intros x y; generalize (compare_spec x y); unfold Cmp, flip.
- destruct (O.compare x y); intuition; try discriminate.
+ intros x y; destruct (compare_spec x y); intuition;
+  try discriminate.
  rewrite H in H0. elim (StrictOrder_Irreflexive y); auto.
  rewrite H in H0. elim (StrictOrder_Irreflexive x); auto.
  Qed.
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v
index 73bd3810f..801c18723 100644
--- a/theories/Structures/OrderedType2Ex.v
+++ b/theories/Structures/OrderedType2Ex.v
@@ -13,174 +13,18 @@
 
 (* $Id$ *)
 
-Require Import OrderedType2 DecidableType2Ex.
-Require Import ZArith NArith Ndec Compare_dec.
+Require Import OrderedType2 NatOrderedType POrderedType NOrderedType
+ ZOrderedType DecidableType2Ex RelationPairs.
 
 (** * Examples of Ordered Type structures. *)
 
-(** First, a particular case of [OrderedType] where
-    the equality is the usual one of Coq. *)
 
-Module Type UsualOrderedType.
- Include Type UsualDecidableType.
-
- Parameter Inline lt : t -> t -> Prop.
- Instance lt_strorder : StrictOrder lt.
- (* The following is useless since eq is Leibniz, but should be there
-    for subtyping... *)
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
-
- Parameter compare : t -> t -> comparison.
- Axiom compare_spec : forall x y, Cmp eq lt (compare x y) x y.
-
-End UsualOrderedType.
-
-(** a [UsualOrderedType] is in particular an [OrderedType]. *)
-
-Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U.
-
-(** [nat] is an ordered type with respect to the usual order on natural numbers. *)
-
-Module Nat_as_OT <: UsualOrderedType.
-
-  Definition t := nat.
-  Definition eq := @eq nat.
-  Definition lt := lt.
-  Definition compare := nat_compare.
-  Definition eq_dec := eq_nat_dec.
-
-  Program Instance eq_equiv : Equivalence eq.
-
-  Instance lt_strorder : StrictOrder lt.
-  Proof.
-  constructor; [exact lt_irrefl|exact lt_trans].
-  Qed.
-
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
-  Proof.
-  unfold eq in *; repeat red; intros; subst; auto.
-  Qed.
-
-  Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y.
-  Proof.
-  intros.
-  unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H.
-  apply nat_compare_eq; auto.
-  apply nat_compare_Lt_lt; auto.
-  apply nat_compare_Gt_gt; auto.
-  Qed.
-
-End Nat_as_OT.
-
-
-(** [Z] is an ordered type with respect to the usual order on integers. *)
-
-Module Z_as_OT <: UsualOrderedType.
-
-  Definition t := Z.
-  Definition eq := @eq Z.
-  Definition lt := Zlt.
-  Definition compare := Zcompare.
-  Definition eq_dec := Z_eq_dec.
-
-  Program Instance eq_equiv : Equivalence eq.
-
-  Instance lt_strorder : StrictOrder lt.
-  Proof.
-  constructor; [exact Zlt_irrefl | exact Zlt_trans].
-  Qed.
-
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
-  Proof.
-  unfold eq in *; repeat red; intros; subst; auto.
-  Qed.
-
-  Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y.
-  Proof.
-  intros.
-  unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H.
-  apply Zcompare_Eq_eq; auto.
-  auto.
-  apply Zgt_lt; auto.
-  Qed.
-
-End Z_as_OT.
-
-(** [positive] is an ordered type with respect to the usual order
-    on natural numbers. *)
-
-Module Positive_as_OT <: UsualOrderedType.
-  Definition t:=positive.
-  Definition eq:=@eq positive.
-  Definition lt:=Plt.
-  Definition compare x y := Pcompare x y Eq.
-
-  Program Instance eq_equiv : Equivalence eq.
-
-  Instance lt_strorder : StrictOrder lt.
-  Proof.
-  constructor; [exact Plt_irrefl | exact Plt_trans].
-  Qed.
-
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
-  Proof.
-  unfold eq in *; repeat red; intros; subst; auto.
-  Qed.
-
-  Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y.
-  Proof.
-  intros.
-  unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H.
-  apply Pcompare_Eq_eq; auto.
-  auto.
-  apply ZC1; auto.
-  Qed.
-
-  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
-  Proof.
-   intros; unfold eq; decide equality.
-  Defined.
-
-End Positive_as_OT.
-
-
-(** [N] is an ordered type with respect to the usual order
-    on natural numbers. *)
-
-Module N_as_OT <: UsualOrderedType.
-  Definition t:=N.
-  Definition eq:=@eq N.
-  Definition lt:=Nlt.
-  Definition compare:=Ncompare.
-
-  Program Instance eq_equiv : Equivalence eq.
-
-  Instance lt_strorder : StrictOrder lt.
-  Proof.
-  constructor; [exact Nlt_irrefl | exact Nlt_trans].
-  Qed.
-
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
-  Proof.
-  unfold eq in *; repeat red; intros; subst; auto.
-  Qed.
-
-  Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y.
-  Proof.
-  intros.
-  unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H.
-  apply Ncompare_Eq_eq; auto.
-  auto.
-  apply Ngt_Nlt; auto.
-  Qed.
-
-  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
-  Proof.
-   intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec.
-  Defined.
-
-End N_as_OT.
+(** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *)
 
+Module Nat_as_OT := NatOrderedType.Nat_as_OT.
+Module Positive_as_OT := POrderedType.Positive_as_OT.
+Module N_as_OT := NOrderedType.N_as_OT.
+Module Z_as_OT := ZOrderedType.Z_as_OT.
 
 (** An OrderedType can now directly be seen as a DecidableType *)
 
@@ -195,21 +39,14 @@ Module Z_as_DT <: UsualDecidableType := Z_as_OT.
 
 
 
-
 (** From two ordered types, we can build a new OrderedType
    over their cartesian product, using the lexicographic order. *)
 
 Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
+ Include PairDecidableType O1 O2.
 
- Definition t := prod O1.t O2.t.
-
- Definition eq := ProdRel O1.eq O2.eq.
-
- Definition lt x y :=
-    O1.lt (fst x) (fst y) \/
-    (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)).
-
- Instance eq_equiv : Equivalence eq.
+ Definition lt :=
+   (relation_disjunction (O1.lt @@ fst) (O1.eq * O2.lt))%signature.
 
  Instance lt_strorder : StrictOrder lt.
  Proof.
@@ -219,7 +56,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
  apply (StrictOrder_Irreflexive x1); auto.
  apply (StrictOrder_Irreflexive x2); intuition.
  (* transitive *)
- intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition.
+ intros (x1,x2) (y1,y2) (z1,z2). compute. intuition.
  left; etransitivity; eauto.
  left; rewrite <- H0; auto.
  left; rewrite H; auto.
@@ -228,8 +65,8 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
 
  Instance lt_compat : Proper (eq==>eq==>iff) lt.
  Proof.
+ compute.
  intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2).
- unfold lt; simpl in *.
  rewrite X1,X2,Y1,Y2; intuition.
  Qed.
 
@@ -240,22 +77,12 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
    | Gt => Gt
   end.
 
- Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y.
+ Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
  Proof.
- intros (x1,x2) (y1,y2); unfold Cmp, flip, compare, eq, lt; simpl.
- generalize (O1.compare_spec x1 y1); destruct (O1.compare x1 y1); intros; auto.
- generalize (O2.compare_spec x2 y2); destruct (O2.compare x2 y2); intros; auto.
+ intros (x1,x2) (y1,y2); unfold compare; simpl.
+ destruct (O1.compare_spec x1 y1); try (constructor; compute; auto).
+ destruct (O2.compare_spec x2 y2); constructor; compute; auto.
  Qed.
 
- Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
- Proof.
- intros; generalize (compare_spec x y); destruct (compare x y).
- left; auto.
- right. intros E; rewrite E in *.
-  apply (StrictOrder_Irreflexive y); auto.
- right. intros E; rewrite E in *.
-  apply (StrictOrder_Irreflexive y); auto.
- Defined.
-
 End PairOrderedType.
 
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v
new file mode 100644
index 000000000..382b6366d
--- /dev/null
+++ b/theories/Structures/OrderedType2Facts.v
@@ -0,0 +1,264 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Import Basics OrderTac.
+Require Export OrderedType2.
+
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+
+(** * Properties of ordered types *)
+
+(** First, an OrderdType (with [<=]) is enough for building an [order]
+    tactic. *)
+
+Module OTF_to_OrderSig (O : OrderedTypeFull) :
+ OrderSig with Definition t := O.t
+          with Definition eq := O.eq
+          with Definition lt := O.lt
+          with Definition le := O.le.
+ Include O.
+ Lemma lt_total : forall x y, O.lt x y \/ O.eq x y \/ O.lt y x.
+ Proof. intros; destruct (O.compare_spec x y); auto. Qed.
+End OTF_to_OrderSig.
+
+
+Module OTF_to_OrderTac (O:OrderedTypeFull).
+ Module OrderElts := OTF_to_OrderSig O.
+ Module OrderTac := MakeOrderTac OrderElts.
+ Ltac order :=
+   change O.eq with OrderElts.eq in *;
+   change O.lt with OrderElts.lt in *;
+   change O.le with OrderElts.le in *;
+   OrderTac.order.
+End OTF_to_OrderTac.
+
+
+(** This allows to prove a few properties of [<=] *)
+
+Module OrderedTypeFullFacts (Import O:OrderedTypeFull).
+
+ Module Order := OTF_to_OrderTac O.
+ Ltac order := Order.order.
+
+ Instance le_compat : Proper (eq==>eq==>iff) le.
+ Proof. repeat red; intuition; order. Qed.
+
+ Instance le_preorder : PreOrder le.
+ Proof. split; red; order. Qed.
+
+ Instance le_order : PartialOrder eq le.
+ Proof. compute; intuition; order. Qed.
+
+ Instance le_antisym : Antisymmetric _ eq le.
+ Proof. apply partial_order_antisym; auto with *. Qed.
+
+ Lemma le_not_gt_iff : forall x y, le x y <-> ~lt y x.
+ Proof. split; order. Qed.
+
+ Lemma lt_not_ge_iff : forall x y, lt x y <-> ~le y x.
+ Proof. split; order. Qed.
+
+ Lemma le_or_gt : forall x y, le x y \/ lt y x.
+ Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
+
+ Lemma lt_or_ge : forall x y, lt x y \/ le y x.
+ Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
+
+ Lemma eq_is_le_ge : forall x y, eq x y <-> le x y /\ le y x.
+ Proof. intuition; order. Qed.
+
+End OrderedTypeFullFacts.
+
+
+(** * Properties of OrderedType *)
+
+Module OrderedTypeFacts (Import O: OrderedType).
+  Module O' := OT_to_Full O.
+  Module Order := OTF_to_OrderTac O'.
+  Ltac order := Order.order.
+
+  Infix "==" := eq (at level 70, no associativity) : order.
+  Infix "<" := lt : order.
+  Notation "x <= y" := (~lt y x) : order.
+  Infix "?=" := compare (at level 70, no associativity) : order.
+
+  Local Open Scope order.
+
+  Tactic Notation "elim_compare" constr(x) constr(y) :=
+   destruct (compare_spec x y).
+
+  Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) :=
+   destruct (compare_spec x y) as [h|h|h].
+
+  (** The following lemmas are either re-phrasing of [eq_equiv] and
+      [lt_strorder] or immediately provable by [order]. Interest:
+      compatibility, test of order, etc *)
+
+  Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x.
+
+  Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y.
+
+  Definition eq_trans (x y z:t) : x==y -> y==z -> x==z :=
+   Equivalence_Transitive x y z.
+
+  Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
+   StrictOrder_Transitive x y z.
+
+  Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
+
+  (** Some more about [compare] *)
+
+  Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x.
+  Proof.
+   intros; rewrite compare_lt_iff; intuition.
+  Qed.
+
+  Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y.
+  Proof.
+   intros; rewrite compare_gt_iff; intuition.
+  Qed.
+
+  Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
+
+  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
+  Proof.
+  intros x x' Hxx' y y' Hyy'.
+  elim_compare x' y'; autorewrite with order; order.
+  Qed.
+
+  Lemma compare_refl : forall x, (x ?= x) = Eq.
+  Proof.
+   intros; elim_compare x x; auto; order.
+  Qed.
+
+  Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
+  Proof.
+   intros; elim_compare x y; autorewrite with order; order.
+  Qed.
+
+  (** For compatibility reasons *)
+  Definition eq_dec := eq_dec.
+
+  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
+  Proof.
+   intros; assert (H:=compare_spec x y); destruct (compare x y);
+    [ right | left | right ]; inversion_clear H; order.
+  Defined.
+
+  Definition eqb x y : bool := if eq_dec x y then true else false.
+
+  Lemma if_eq_dec : forall x y (B:Type)(b b':B),
+    (if eq_dec x y then b else b') =
+    (match compare x y with Eq => b | _ => b' end).
+  Proof.
+  intros; destruct eq_dec; elim_compare x y; auto; order.
+  Qed.
+
+  Lemma eqb_alt :
+    forall x y, eqb x y = match compare x y with Eq => true | _ => false end.
+  Proof.
+  unfold eqb; intros; apply if_eq_dec.
+  Qed.
+
+  Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb.
+  Proof.
+  intros x x' Hxx' y y' Hyy'.
+  rewrite 2 eqb_alt, Hxx', Hyy'; auto.
+  Qed.
+
+End OrderedTypeFacts.
+
+
+
+
+
+
+(** * Tests of the order tactic
+
+    Is it at least capable of proving some basic properties ? *)
+
+Module OrderedTypeTest (O:OrderedType).
+  Module Import MO := OrderedTypeFacts O.
+  Local Open Scope order.
+  Lemma lt_not_eq x y : x<y -> ~x==y.  Proof. order. Qed.
+  Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed.
+  Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed.
+  Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed.
+  Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed.
+  Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed.
+  Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed.
+  Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed.
+  Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed.
+  Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed.
+  Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed.
+  Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed.
+  Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed.
+  Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed.
+  Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed.
+  Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed.
+  Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed.
+  Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed.
+  Lemma eq_is_nlt_ngt x y : x==y <-> ~x<y /\ ~y<x.
+  Proof. intuition; order. Qed.
+End OrderedTypeTest.
+
+
+
+(** * Reversed OrderedTypeFull.
+
+   we can switch the orientation of the order. This is used for
+   example when deriving properties of [min] out of the ones of [max]
+   (see [GenericMinMax]).
+*)
+
+Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
+
+Definition t := O.t.
+Definition eq := O.eq.
+Instance eq_equiv : Equivalence eq.
+Definition eq_dec := O.eq_dec.
+
+Definition lt := flip O.lt.
+Definition le := flip O.le.
+
+Instance lt_strorder: StrictOrder lt.
+Proof. unfold lt; auto with *. Qed.
+Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Proof. unfold lt; auto with *. Qed.
+
+Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
+
+Definition compare := flip O.compare.
+
+Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+Proof.
+intros; unfold compare, eq, lt, flip.
+destruct (O.compare_spec y x); auto.
+Qed.
+
+End OrderedTypeRev.
+
diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v
new file mode 100644
index 000000000..4aa07dfdc
--- /dev/null
+++ b/theories/Structures/OrderedType2Lists.v
@@ -0,0 +1,264 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Export RelationPairs SetoidList OrderedType2.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Specialization of results about lists modulo. *)
+
+Module OrderedTypeLists (Import O:OrderedType).
+
+Section ForNotations.
+
+Notation In:=(InA eq).
+Notation Inf:=(lelistA lt).
+Notation Sort:=(sort lt).
+Notation NoDup:=(NoDupA eq).
+
+Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+Proof. intros. rewrite <- H; auto. Qed.
+
+Lemma ListIn_In : forall l x, List.In x l -> In x l.
+Proof. exact (In_InA eq_equiv). Qed.
+
+Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_ltA lt_strorder). Qed.
+
+Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+
+Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
+Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
+
+Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
+Proof. exact (@In_InfA t lt). Qed.
+
+Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
+Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
+
+Lemma Inf_alt :
+ forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
+Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
+
+Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
+Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed.
+
+End ForNotations.
+
+Hint Resolve ListIn_In Sort_NoDup Inf_lt.
+Hint Immediate In_eq Inf_lt.
+
+End OrderedTypeLists.
+
+
+
+
+
+(** * Results about keys and data as manipulated in FMaps. *)
+
+
+Module KeyOrderedType(Import O:OrderedType).
+ Module Import MO:=OrderedTypeLists(O).
+
+ Section Elt.
+ Variable elt : Type.
+ Notation key:=t.
+
+  Local Open Scope signature_scope.
+
+  Definition eqk : relation (key*elt) := eq @@ fst.
+  Definition eqke : relation (key*elt) := eq * Logic.eq.
+  Definition ltk : relation (key*elt) := lt @@ fst.
+
+  Hint Unfold eqk eqke ltk.
+
+  (* eqke is stricter than eqk *)
+
+  Global Instance eqke_eqk : subrelation eqke eqk.
+  Proof. firstorder. Qed.
+
+  (* eqk, eqke are equalities, ltk is a strict order *)
+
+  Global Instance eqk_equiv : Equivalence eqk.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+
+  Global Instance ltk_strorder : StrictOrder ltk.
+
+  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
+  Proof. unfold eqk, ltk; auto with *. Qed.
+
+  (* Additionnal facts *)
+
+  Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt).
+  Proof. apply pair_compat. Qed.
+
+  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
+  Proof.
+  intros e e' LT EQ; rewrite EQ in LT.
+  elim (StrictOrder_Irreflexive _ LT).
+  Qed.
+
+  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
+  Proof.
+  intros e e' LT EQ; rewrite EQ in LT.
+  elim (StrictOrder_Irreflexive _ LT).
+  Qed.
+
+  Lemma InA_eqke_eqk :
+     forall x m, InA eqke x m -> InA eqk x m.
+  Proof.
+    unfold eqke, RelProd; induction 1; firstorder.
+  Qed.
+  Hint Resolve InA_eqke_eqk.
+
+  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
+  Definition In k m := exists e:elt, MapsTo k e m.
+  Notation Sort := (sort ltk).
+  Notation Inf := (lelistA ltk).
+
+  Hint Unfold MapsTo In.
+
+  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+
+  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
+  Proof.
+  firstorder.
+  exists x; auto.
+  induction H.
+  destruct y; compute in H.
+  exists e; left; auto.
+  destruct IHInA as [e H0].
+  exists e; auto.
+  Qed.
+
+  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
+  Proof.
+  unfold In, MapsTo.
+  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
+  firstorder.
+  exists (snd x), x; auto.
+  Qed.
+
+  Lemma In_nil : forall k, In k nil <-> False.
+  Proof.
+  intros; rewrite In_alt2; apply Exists_nil.
+  Qed.
+
+  Lemma In_cons : forall k p l,
+   In k (p::l) <-> eq k (fst p) \/ In k l.
+  Proof.
+  intros; rewrite !In_alt2, Exists_cons; intuition.
+  Qed.
+
+  Global Instance MapsTo_compat :
+   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
+  Proof.
+  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
+  rewrite Hx, He, Hl; intuition.
+  Qed.
+
+  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
+  Proof.
+  intros x x' Hx l l' Hl. rewrite !In_alt.
+  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
+
+  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
+  Proof. intros l x x' H. rewrite H; auto. Qed.
+
+  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
+  Proof. apply InfA_ltA; auto with *. Qed.
+
+  Hint Immediate Inf_eq.
+  Hint Resolve Inf_lt.
+
+  Lemma Sort_Inf_In :
+      forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
+  Proof. apply SortA_InfA_InA; auto with *. Qed.
+
+  Lemma Sort_Inf_NotIn :
+      forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
+  Proof.
+    intros; red; intros.
+    destruct H1 as [e' H2].
+    elim (@ltk_not_eqk (k,e) (k,e')).
+    eapply Sort_Inf_In; eauto.
+    red; simpl; auto.
+  Qed.
+
+  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
+  Proof. apply SortA_NoDupA; auto with *. Qed.
+
+  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
+  Proof.
+   intros; invlist sort; eapply Sort_Inf_In; eauto.
+  Qed.
+
+  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
+      ltk e e' \/ eqk e e'.
+  Proof.
+    intros; invlist InA; auto.
+    left; apply Sort_In_cons_1 with l; auto.
+  Qed.
+
+  Lemma Sort_In_cons_3 :
+    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
+  Proof.
+    intros; invlist sort; red; intros.
+    eapply Sort_Inf_NotIn; eauto using In_eq.
+  Qed.
+
+  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
+  Proof.
+    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
+    right; exists x; auto.
+  Qed.
+
+  Lemma In_inv_2 : forall k k' e e' l,
+      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
+  Proof.
+   intros; invlist InA; intuition.
+  Qed.
+
+  Lemma In_inv_3 : forall x x' l,
+      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+  Proof.
+   intros; invlist InA; compute in * |- ; intuition.
+  Qed.
+
+ End Elt.
+
+ Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqk_equiv elt)).
+ Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqk_equiv elt)).
+ Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqk_equiv elt)).
+ Hint Resolve (fun elt => @Equivalence_Reflexive _ _ (eqke_equiv elt)).
+ Hint Resolve (fun elt => @Equivalence_Transitive _ _ (eqke_equiv elt)).
+ Hint Immediate (fun elt => @Equivalence_Symmetric _ _ (eqke_equiv elt)).
+ Hint Resolve (fun elt => @StrictOrder_Transitive _ _ (ltk_strorder elt)).
+
+ Hint Unfold eqk eqke ltk.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve ltk_not_eqk ltk_not_eqke.
+ Hint Resolve InA_eqke_eqk.
+ Hint Unfold MapsTo In.
+ Hint Immediate Inf_eq.
+ Hint Resolve Inf_lt.
+ Hint Resolve Sort_Inf_NotIn.
+ Hint Resolve In_inv_2 In_inv_3.
+
+End KeyOrderedType.
+