Imported Upstream snapshot 8.3~beta0+13298

15 files changed, 3711 insertions, 0 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
new file mode 100644
index 00000000..2c72e30b
--- /dev/null
+++ b/theories/Structures/DecidableType.v
@@ -0,0 +1,156 @@
+(***********************************************************************)
+(*  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$ *)
+
+Require Export SetoidList.
+Require Equalities.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** NB: This file is here only for compatibility with earlier version of
+    [FSets] and [FMap]. Please use [Structures/Equalities.v] directly now. *)
+
+(** * Types with Equalities, and nothing more (for subtyping purpose) *)
+
+Module Type EqualityType := Equalities.EqualityTypeOrig.
+
+(** * Types with decidable Equalities (but no ordering) *)
+
+Module Type DecidableType := Equalities.DecidableTypeOrig.
+
+(** * 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 *)
+
+  Lemma eqk_refl : forall e, eqk e e.
+  Proof. auto. Qed.
+
+  Lemma eqke_refl : forall e, eqke e e.
+  Proof. auto. Qed.
+
+  Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.
+  Proof. auto. Qed.
+
+  Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.
+  Proof. unfold eqke; intuition. Qed.
+
+  Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
+  Proof. eauto. Qed.
+
+  Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
+  Proof.
+    unfold eqke; intuition; [ eauto | congruence ].
+  Qed.
+
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+  Hint Immediate eqk_sym eqke_sym.
+
+  Global Instance eqk_equiv : Equivalence eqk.
+  Proof. split; eauto. Qed.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+  Proof. split; eauto. Qed.
+
+  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; apply InA_eqA with p; auto with *.
+  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.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
+  Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof.
+  destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
+  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 Unfold eqk eqke.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+ Hint Immediate eqk_sym eqke_sym.
+ Hint Resolve InA_eqke_eqk.
+ Hint Unfold MapsTo In.
+ Hint Resolve In_inv_2 In_inv_3.
+
+End KeyDecidableType.
+
+
+
+
+
diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v
new file mode 100644
index 00000000..4407ead4
--- /dev/null
+++ b/theories/Structures/DecidableTypeEx.v
@@ -0,0 +1,96 @@
+(***********************************************************************)
+(*  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$ *)
+
+Require Import DecidableType OrderedType OrderedTypeEx.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** NB: This file is here only for compatibility with earlier version of
+    [FSets] and [FMap]. Please use [Structures/Equalities.v] directly now. *)
+
+(** * Examples of Decidable Type structures. *)
+
+(** A particular case of [DecidableType] where
+    the equality is the usual one of Coq. *)
+
+Module Type UsualDecidableType := Equalities.UsualDecidableTypeOrig.
+
+(** 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 := Equalities.MiniDecidableType.
+
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType
+ := Equalities.Make_UDT M.
+
+(** An OrderedType can now directly be seen as a DecidableType *)
+
+Module OT_as_DT (O:OrderedType) <: DecidableType := O.
+
+(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *)
+
+Module Nat_as_DT <: UsualDecidableType := Nat_as_OT.
+Module Positive_as_DT <: UsualDecidableType := Positive_as_OT.
+Module N_as_DT <: UsualDecidableType := N_as_OT.
+Module Z_as_DT <: UsualDecidableType := Z_as_OT.
+
+(** 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 eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y).
+
+ Lemma eq_refl : forall x : t, eq x x.
+ Proof.
+ intros (x1,x2); red; simpl; auto.
+ Qed.
+
+ Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+ Proof.
+ intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
+ Qed.
+
+ Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+ Proof.
+ 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.
+ Defined.
+
+End PairDecidableType.
+
+(** Similarly for pairs of UsualDecidableType *)
+
+Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
+ Definition t := prod D1.t D2.t.
+ Definition eq := @eq t.
+ Definition eq_refl := @refl_equal t.
+ Definition eq_sym := @sym_eq t.
+ Definition eq_trans := @trans_eq t.
+ Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
+ Proof.
+ intros (x1,x2) (y1,y2);
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+ unfold eq, D1.eq, D2.eq in *; simpl;
+ (left; f_equal; auto; fail) ||
+ (right; intro H; injection H; auto).
+ Defined.
+
+End PairUsualDecidableType.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
new file mode 100644
index 00000000..487b1d0c
--- /dev/null
+++ b/theories/Structures/Equalities.v
@@ -0,0 +1,218 @@
+(***********************************************************************)
+(*  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$ *)
+
+Require Export RelationClasses.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Structure with just a base type [t] *)
+
+Module Type Typ.
+  Parameter Inline t : Type.
+End Typ.
+
+(** * Structure with an equality relation [eq] *)
+
+Module Type HasEq (Import T:Typ).
+  Parameter Inline eq : t -> t -> Prop.
+End HasEq.
+
+Module Type Eq := Typ <+ HasEq.
+
+Module Type EqNotation (Import E:Eq).
+  Infix "==" := eq (at level 70, no associativity).
+  Notation "x ~= y" := (~eq x y) (at level 70, no associativity).
+End EqNotation.
+
+Module Type Eq' := Eq <+ EqNotation.
+
+(** * Specification of the equality via the [Equivalence] type class *)
+
+Module Type IsEq (Import E:Eq).
+  Declare Instance eq_equiv : Equivalence eq.
+End IsEq.
+
+(** * Earlier specification of equality by three separate lemmas. *)
+
+Module Type IsEqOrig (Import E:Eq').
+  Axiom eq_refl : forall x : t, x==x.
+  Axiom eq_sym : forall x y : t, x==y -> y==x.
+  Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
+  Hint Immediate eq_sym.
+  Hint Resolve eq_refl eq_trans.
+End IsEqOrig.
+
+(** * Types with decidable equality *)
+
+Module Type HasEqDec (Import E:Eq').
+  Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }.
+End HasEqDec.
+
+(** * Boolean Equality *)
+
+(** Having [eq_dec] is the same as having a boolean equality plus
+    a correctness proof. *)
+
+Module Type HasEqBool (Import E:Eq').
+  Parameter Inline eqb : t -> t -> bool.
+  Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
+End HasEqBool.
+
+(** From these basic blocks, we can build many combinations
+    of static standalone module types. *)
+
+Module Type EqualityType := Eq <+ IsEq.
+
+Module Type EqualityTypeOrig := Eq <+ IsEqOrig.
+
+Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig
+ := Eq <+ IsEq <+ IsEqOrig.
+
+Module Type DecidableType <: EqualityType
+ := Eq <+ IsEq <+ HasEqDec.
+
+Module Type DecidableTypeOrig <: EqualityTypeOrig
+ := Eq <+ IsEqOrig <+ HasEqDec.
+
+Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig
+ := EqualityTypeBoth <+ HasEqDec.
+
+Module Type BooleanEqualityType <: EqualityType
+ := Eq <+ IsEq <+ HasEqBool.
+
+Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType
+ := Eq <+ IsEq <+ HasEqDec <+ HasEqBool.
+
+Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType
+ := Eq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+
+(** Same, with notation for [eq] *)
+
+Module Type EqualityType' := EqualityType <+ EqNotation.
+Module Type EqualityTypeOrig' := EqualityTypeOrig <+ EqNotation.
+Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation.
+Module Type DecidableType' := DecidableType <+ EqNotation.
+Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation.
+Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation.
+Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation.
+Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation.
+Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
+
+(** * Compatibility wrapper from/to the old version of
+      [EqualityType] and [DecidableType] *)
+
+Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
+ Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
+End BackportEq.
+
+Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
+ Instance eq_equiv : Equivalence E.eq.
+ Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
+End UpdateEq.
+
+Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
+ := E <+ BackportEq.
+
+Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth
+ := E <+ UpdateEq.
+
+Module Backport_DT (E:DecidableType) <: DecidableTypeBoth
+ := E <+ BackportEq.
+
+Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth
+ := E <+ UpdateEq.
+
+
+(** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
+
+Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E.
+ Definition eqb x y := if F.eq_dec x y then true else false.
+ Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
+ Proof.
+  intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ].
+  auto with *.
+  split. discriminate. intro EQ; elim NEQ; auto.
+ Qed.
+End HasEqDec2Bool.
+
+Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E.
+ Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
+ Proof.
+  intros x y. assert (H:=F.eqb_eq x y).
+  destruct (F.eqb x y); [left|right].
+  apply -> H; auto.
+  intro EQ. apply H in EQ. discriminate.
+ Defined.
+End HasEqBool2Dec.
+
+Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
+ := E <+ HasEqDec2Bool.
+
+Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
+ := E <+ HasEqBool2Dec.
+
+
+
+(** * UsualDecidableType
+
+   A particular case of [DecidableType] where the equality is
+   the usual one of Coq. *)
+
+Module Type HasUsualEq (Import T:Typ) <: HasEq T.
+ Definition eq := @Logic.eq t.
+End HasUsualEq.
+
+Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
+
+Module Type UsualIsEq (E:UsualEq) <: IsEq E.
+ (* No Instance syntax to avoid saturating the Equivalence tables *)
+ Lemma eq_equiv : Equivalence E.eq.
+ Proof. exact eq_equivalence. Qed.
+End UsualIsEq.
+
+Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
+ Definition eq_refl := @Logic.eq_refl E.t.
+ Definition eq_sym := @Logic.eq_sym E.t.
+ Definition eq_trans := @Logic.eq_trans E.t.
+End UsualIsEqOrig.
+
+Module Type UsualEqualityType <: EqualityType
+ := UsualEq <+ UsualIsEq.
+
+Module Type UsualDecidableType <: DecidableType
+ := UsualEq <+ UsualIsEq <+ HasEqDec.
+
+Module Type UsualDecidableTypeOrig <: DecidableTypeOrig
+ := UsualEq <+ UsualIsEqOrig <+ HasEqDec.
+
+Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec.
+
+Module Type UsualBoolEq := UsualEq <+ HasEqBool.
+
+Module Type UsualDecidableTypeFull <: DecidableTypeFull
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec <+ HasEqBool.
+
+
+(** Some shortcuts for easily building a [UsualDecidableType] *)
+
+Module Type MiniDecidableType.
+ Include Typ.
+ Parameter eq_dec : forall x y : t, {x=y}+{~x=y}.
+End MiniDecidableType.
+
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth
+ := M <+ HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
+
+Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
+ := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
new file mode 100644
index 00000000..d9b1d76f
--- /dev/null
+++ b/theories/Structures/EqualitiesFacts.v
@@ -0,0 +1,185 @@
+(***********************************************************************)
+(*  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 Equalities Bool SetoidList RelationPairs.
+
+(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
+
+Module BoolEqualityFacts (Import E : BooleanEqualityType).
+
+Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
+Proof.
+intros x x' Exx' y y' Eyy'.
+apply eq_true_iff_eq.
+rewrite 2 eqb_eq, Exx', Eyy'; auto with *.
+Qed.
+
+End BoolEqualityFacts.
+
+
+(** * Keys and datas used in FMap *)
+Module KeyDecidableType(Import D:DecidableType).
+
+ Section Elt.
+ Variable elt : Type.
+ Notation key:=t.
+
+  Local Open Scope signature_scope.
+
+  Definition eqk : relation (key*elt) := eq @@1.
+  Definition eqke : relation (key*elt) := eq * Logic.eq.
+  Hint Unfold eqk eqke.
+
+  (* 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.
+
+  (* Additionnal facts *)
+
+  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.
+
+  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; 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 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 Unfold eqk eqke.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve InA_eqke_eqk.
+ Hint Unfold MapsTo In.
+ Hint Resolve In_inv_2 In_inv_3.
+
+End KeyDecidableType.
+
+
+(** * PairDecidableType 
+   
+   From two decidable types, we can build a new DecidableType
+   over their cartesian product. *)
+
+Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
+
+ Definition t := (D1.t * D2.t)%type.
+
+ Definition eq := (D1.eq * D2.eq)%signature.
+
+ Instance eq_equiv : Equivalence eq.
+
+ 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);
+  compute; intuition.
+ Defined.
+
+End PairDecidableType.
+
+(** Similarly for pairs of UsualDecidableType *)
+
+Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
+ 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 }.
+ Proof.
+ intros (x1,x2) (y1,y2);
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+ unfold eq, D1.eq, D2.eq in *; simpl;
+ (left; f_equal; auto; fail) ||
+ (right; intro H; injection H; auto).
+ Defined.
+
+End PairUsualDecidableType.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
new file mode 100644
index 00000000..68f20189
--- /dev/null
+++ b/theories/Structures/GenericMinMax.v
@@ -0,0 +1,656 @@
+(***********************************************************************)
+(*  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 Orders OrdersTac OrdersFacts Setoid Morphisms Basics.
+
+(** * A Generic construction of min and max *)
+
+(** ** First, an interface for types with [max] and/or [min] *)
+
+Module Type HasMax (Import E:EqLe').
+ Parameter Inline max : t -> t -> t.
+ Parameter max_l : forall x y, y<=x -> max x y == x.
+ Parameter max_r : forall x y, x<=y -> max x y == y.
+End HasMax.
+
+Module Type HasMin (Import E:EqLe').
+ Parameter Inline min : t -> t -> t.
+ Parameter min_l : forall x y, x<=y -> min x y == x.
+ Parameter min_r : forall x y, y<=x -> min x y == y.
+End HasMin.
+
+Module Type HasMinMax (E:EqLe) := HasMax E <+ HasMin E.
+
+
+(** ** 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 ge_not_lt : forall x y, y<=x -> x<y -> False.
+ Proof.
+ intros x y H H'.
+ apply (StrictOrder_Irreflexive x).
+ rewrite le_lteq in *; destruct H as [H|H].
+ transitivity y; auto.
+ rewrite H in H'; auto.
+ Qed.
+
+ Lemma max_l : forall x y, y<=x -> max x y == x.
+ Proof.
+ intros. unfold max, gmax. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt x y); auto.
+ Qed.
+
+ Lemma max_r : forall x y, x<=y -> max x y == y.
+ Proof.
+ intros. unfold max, gmax. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt y x); auto.
+ Qed.
+
+ Lemma min_l : forall x y, x<=y -> min x y == x.
+ Proof.
+ intros. unfold min, gmin. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt y x); auto.
+ Qed.
+
+ Lemma min_r : forall x y, y<=x -> min x y == y.
+ Proof.
+ intros. unfold min, gmin. case compare_spec; auto with relations.
+ intros; elim (ge_not_lt x y); auto.
+ Qed.
+
+End GenericMinMax.
+
+
+(** ** Consequences of the minimalist interface: facts about [max]. *)
+
+Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
+ Module Import T := !MakeOrderTac O.
+
+(** An alternative caracterisation of [max], equivalent to
+    [max_l /\ max_r] *)
+
+Lemma max_spec : forall n m,
+  (n < m /\ max n m == m)  \/ (m <= n /\ max n m == n).
+Proof.
+ intros n m.
+ destruct (lt_total n m); [left|right].
+ split; auto. apply max_r. rewrite le_lteq; auto.
+ assert (m <= n) by (rewrite le_lteq; intuition).
+ split; auto. apply max_l; auto.
+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.
+
+Instance : Proper (eq==>eq==>iff) le.
+Proof. repeat red. intuition order. Qed.
+
+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 (lt_total x y); intuition order.
+Qed.
+
+
+(** A 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 (lt_total 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.
+
+(** [max] commutes with monotone functions. *)
+
+Lemma max_mono: 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 (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (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 (max_spec n n); intuition.
+Qed.
+
+Notation max_idempotent := max_id (only parsing).
+
+Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p.
+Proof.
+ intros.
+ destruct (max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'.
+ destruct (max_spec m p); intuition; order. order.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order.
+ destruct (max_spec m p); intuition; order.
+Qed.
+
+Lemma max_comm : forall n m, max n m == max m n.
+Proof.
+ intros.
+ destruct (max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
+ destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
+Qed.
+
+(** *** Least-upper bound properties of [max] *)
+
+Lemma le_max_l : forall n m, n <= max n m.
+Proof.
+ intros; destruct (max_spec n m); intuition; order.
+Qed.
+
+Lemma le_max_r : forall n m, m <= max n m.
+Proof.
+ intros; destruct (max_spec n m); intuition; order.
+Qed.
+
+Lemma max_l_iff : forall n m, max n m == n <-> m <= n.
+Proof.
+ split. intro H; rewrite <- H. apply le_max_r. apply max_l.
+Qed.
+
+Lemma max_r_iff : forall n m, max n m == m <-> n <= m.
+Proof.
+ split. intro H; rewrite <- H. apply le_max_l. apply max_r.
+Qed.
+
+Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m.
+Proof.
+ intros n m p H; destruct (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 (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 (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 (max_spec n m); intuition; order.
+Qed.
+
+Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
+Proof.
+ intros; destruct (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 (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 (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 (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 (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 (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 MaxLogicalProperties.
+
+
+(** ** Properties concernant [min], then both [min] and [max].
+
+   To avoid too much code duplication, we exploit that [min] can be
+   seen as a [max] of the reversed order.
+*)
+
+Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
+ Include MaxLogicalProperties O M.
+ Import T.
+
+ Module ORev := TotalOrderRev O.
+ Module MRev <: HasMax ORev.
+  Definition max x y := M.min y x.
+  Definition max_l x y := M.min_r y x.
+  Definition max_r x y := M.min_l y x.
+ End MRev.
+ Module MPRev := MaxLogicalProperties 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. intros. exact (MPRev.max_spec m n). 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_mono: 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_mono; 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.
+
+Notation min_idempotent := min_id (only parsing).
+
+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 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_l_iff : forall n m, min n m == n <-> n <= m.
+Proof. intros n m. exact (MPRev.max_r_iff m n). Qed.
+
+Lemma min_r_iff : forall n m, min n m == m <-> m <= n.
+Proof. intros n m. exact (MPRev.max_l_iff 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 (min_spec n m) as [(C,E)|(C,E)]; rewrite E.
+ apply max_l. order.
+ destruct (max_spec n m); intuition; order.
+Qed.
+
+Lemma max_min_absorption : forall n m, min n (max n m) == n.
+Proof.
+ intros.
+ destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E.
+ destruct (min_spec n m) as [(C',E')|(C',E')]; auto. order.
+ apply min_l; auto. 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_mono.
+ 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_mono.
+ 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 with *.
+ destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'.
+ rewrite 2 max_l; try order. rewrite min_le_iff; auto.
+ rewrite 2 max_l; try 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 with *.
+ destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'.
+ rewrite 2 min_l; try order. rewrite max_le_iff; right; order.
+ rewrite 2 min_l; try 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_antimono : 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 (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f y <= f x) by (apply Lef; order). order.
+ assert (f x <= f y) by (apply Lef; order). order.
+Qed.
+
+Lemma min_max_antimono : 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 (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f y <= f x) by (apply Lef; order). order.
+ assert (f x <= f y) by (apply Lef; order). order.
+Qed.
+
+End MinMaxLogicalProperties.
+
+
+(** ** Properties requiring a decidable order *)
+
+Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
+
+(** 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.
+destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
+assert (n<=m) by (rewrite le_lteq; auto).
+apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
+assert (n<=m) by (rewrite le_lteq; auto).
+apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
+assert (m<=n) by (rewrite le_lteq; auto).
+apply (Compat n), Hl; auto. symmetry; apply max_l; auto.
+Defined.
+
+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 with relations.
+ intros x y H [E|E]; [left|right]; rewrite <-H; auto.
+Defined.
+
+(** Idem for [min] *)
+
+Lemma min_case_strong : forall n m (P:O.t -> Type),
+ (forall x y, x == y -> P x -> P y) ->
+ (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
+Proof.
+intros n m P Compat Hl Hr.
+destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
+assert (n<=m) by (rewrite le_lteq; auto).
+apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
+assert (n<=m) by (rewrite le_lteq; auto).
+apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
+assert (m<=n) by (rewrite le_lteq; auto).
+apply (Compat m), Hr; auto. symmetry; apply min_r; auto.
+Defined.
+
+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. apply min_case; auto with relations.
+ intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations.
+Defined.
+
+End MinMaxDecProperties.
+
+Module MinMaxProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
+ Module OT := OTF_to_TotalOrder O.
+ Include MinMaxLogicalProperties OT M.
+ Include MinMaxDecProperties O M.
+ Definition max_l := max_l.
+ Definition max_r := max_r.
+ Definition min_l := min_l.
+ Definition min_r := min_r.
+ Notation max_monotone := max_mono.
+ Notation min_monotone := min_mono.
+ Notation max_min_antimonotone := max_min_antimono.
+ Notation min_max_antimonotone := min_max_antimono.
+End MinMaxProperties.
+
+
+(** ** When the equality is Leibniz, we can skip a few [Proper] precondition. *)
+
+Module UsualMinMaxLogicalProperties
+ (Import O:UsualTotalOrder')(Import M:HasMinMax O).
+
+ Include MinMaxLogicalProperties O M.
+
+ Lemma max_monotone : forall f, Proper (le ==> le) f ->
+  forall x y, max (f x) (f y) = f (max x y).
+ Proof. intros; apply max_mono; auto. congruence. Qed.
+
+ Lemma min_monotone : forall f, Proper (le ==> le) f ->
+  forall x y, min (f x) (f y) = f (min x y).
+ Proof. intros; apply min_mono; auto. congruence. Qed.
+
+ Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f ->
+  forall x y, min (f x) (f y) = f (max x y).
+ Proof. intros; apply min_max_antimono; auto. congruence. Qed.
+
+ Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f ->
+  forall x y, max (f x) (f y) = f (min x y).
+ Proof. intros; apply max_min_antimono; auto. congruence. Qed.
+
+End UsualMinMaxLogicalProperties.
+
+
+Module UsualMinMaxDecProperties
+ (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
+
+ Module P := MinMaxDecProperties O M.
+
+ Lemma max_case_strong : forall n m (P:t -> Type),
+  (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
+ Proof. intros; apply P.max_case_strong; auto. congruence. Defined.
+
+ Lemma max_case : forall n m (P:t -> Type),
+  P n -> P m -> P (max n m).
+ Proof. intros; apply max_case_strong; auto. Defined.
+
+ Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
+ Proof. exact P.max_dec. Defined.
+
+ Lemma min_case_strong : forall n m (P:O.t -> Type),
+  (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
+ Proof. intros; apply P.min_case_strong; auto. congruence. Defined.
+
+ Lemma min_case : forall n m (P:O.t -> Type),
+  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. exact P.min_dec. Defined.
+
+End UsualMinMaxDecProperties.
+
+Module UsualMinMaxProperties
+ (Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
+ Module OT := OTF_to_TotalOrder O.
+ Include UsualMinMaxLogicalProperties OT M.
+ Include UsualMinMaxDecProperties O M.
+ Definition max_l := max_l.
+ Definition max_r := max_r.
+ Definition min_l := min_l.
+ Definition min_r := min_r.
+End UsualMinMaxProperties.
+
+
+(** From [TotalOrder] and [HasMax] and [HasEqDec], we can prove
+    that the order is decidable and build an [OrderedTypeFull]. *)
+
+Module TOMaxEqDec_to_Compare
+ (Import O:TotalOrder')(Import M:HasMax O)(Import E:HasEqDec O) <: HasCompare O.
+
+ Definition compare x y :=
+  if eq_dec x y then Eq
+  else if eq_dec (M.max x y) y then Lt else Gt.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+ intros; unfold compare; repeat destruct eq_dec; auto; constructor.
+ destruct (lt_total x y); auto.
+ absurd (x==y); auto. transitivity (max x y); auto.
+ symmetry. apply max_l. rewrite le_lteq; intuition.
+ destruct (lt_total y x); auto.
+ absurd (max x y == y); auto. apply max_r; rewrite le_lteq; intuition.
+ Qed.
+
+End TOMaxEqDec_to_Compare.
+
+Module TOMaxEqDec_to_OTF (O:TotalOrder)(M:HasMax O)(E:HasEqDec O)
+ <: OrderedTypeFull
+ := O <+ E <+ TOMaxEqDec_to_Compare O M E.
+
+
+
+(** TODO: 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 ?
+
+*)
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
new file mode 100644
index 00000000..72fbe796
--- /dev/null
+++ b/theories/Structures/OrderedType.v
@@ -0,0 +1,485 @@
+(***********************************************************************)
+(*  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$ *)
+
+Require Export SetoidList Morphisms OrdersTac.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** NB: This file is here only for compatibility with earlier version of
+     [FSets] and [FMap]. Please use [Structures/Orders.v] directly now. *)
+
+(** * Ordered types *)
+
+Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
+  | 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 MiniOrderedType.
+
+  Parameter Inline t : Type.
+
+  Parameter Inline eq : t -> t -> Prop.
+  Parameter Inline lt : 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.
+
+  Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+  Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+
+  Parameter compare : forall x y : t, Compare lt eq x y.
+
+  Hint Immediate eq_sym.
+  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
+
+End MiniOrderedType.
+
+Module Type OrderedType.
+  Include MiniOrderedType.
+
+  (** A [eq_dec] can be deduced from [compare] below. But adding this
+     redundant field allows to see an OrderedType as a DecidableType. *)
+  Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+
+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; elim (compare x y); intro H; [ right | left | right ]; auto.
+   assert (~ eq y x); auto.
+  Defined.
+
+End MOT_to_OT.
+
+(** * Ordered types properties *)
+
+(** Additional properties that can be derived from signature
+    [OrderedType]. *)
+
+Module OrderedTypeFacts (Import O: OrderedType).
+
+  Instance eq_equiv : Equivalence eq.
+  Proof. split; [ exact eq_refl | exact eq_sym | exact eq_trans ]. Qed.
+
+  Lemma lt_antirefl : forall x, ~ lt x x.
+  Proof.
+   intros; intro; absurd (eq x x); auto.
+  Qed.
+
+  Instance lt_strorder : StrictOrder lt.
+  Proof. split; [ exact lt_antirefl | exact lt_trans]. Qed.
+
+  Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
+  Proof.
+   intros; destruct (compare x z); auto.
+   elim (lt_not_eq H); apply eq_trans with z; auto.
+   elim (lt_not_eq (lt_trans l H)); auto.
+  Qed.
+
+  Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
+  Proof.
+   intros; destruct (compare x z); auto.
+   elim (lt_not_eq H0); apply eq_trans with x; auto.
+   elim (lt_not_eq (lt_trans H0 l)); auto.
+  Qed.
+
+  Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Proof.
+  apply proper_sym_impl_iff_2; auto with *.
+  intros x x' Hx y y' Hy H.
+  apply eq_lt with x; auto.
+  apply lt_eq with y; auto.
+  Qed.
+
+  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 <: Orders.TotalOrder.
+  Definition t := t.
+  Definition eq := eq.
+  Definition lt := lt.
+  Definition le x y := lt x y \/ eq x y.
+  Definition eq_equiv := eq_equiv.
+  Definition lt_strorder := lt_strorder.
+  Definition lt_compat := lt_compat.
+  Definition lt_total := lt_total.
+  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 := OrderTac.order.
+
+  Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed.
+  Lemma eq_le x y z : eq x y -> ~lt y z -> ~lt x z. Proof. order. Qed.
+  Lemma neq_eq x y z : ~eq x y -> eq y z -> ~eq x z. Proof. order. Qed.
+  Lemma eq_neq x y z : eq x y -> ~eq y z -> ~eq x z. Proof. order. Qed.
+  Lemma le_lt_trans x y z : ~lt y x -> lt y z -> lt x z. Proof. order. Qed.
+  Lemma lt_le_trans x y z : lt x y -> ~lt z y -> lt x z. Proof. order. Qed.
+  Lemma le_neq x y : ~lt x y -> ~eq x y -> lt y x. Proof. order. Qed.
+  Lemma le_trans x y z : ~lt y x -> ~lt z y -> ~lt z x. Proof. order. Qed.
+  Lemma le_antisym x y : ~lt y x -> ~lt x y -> eq x y. Proof. order. Qed.
+  Lemma neq_sym x y : ~eq x y -> ~eq y x. Proof. order. Qed.
+  Lemma lt_le x y : lt x y -> ~lt y x. Proof. order. Qed.
+  Lemma gt_not_eq x y : lt y x -> ~ eq x y. Proof. order. Qed.
+  Lemma eq_not_lt x y : eq x y -> ~ lt x y. Proof. order. Qed.
+  Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed.
+  Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed.
+
+  Hint Resolve gt_not_eq eq_not_lt.
+  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
+  Hint Resolve eq_not_gt lt_antirefl lt_not_gt.
+
+  Lemma elim_compare_eq :
+   forall x y : t,
+   eq x y -> exists H : eq x y, compare x y = EQ _ H.
+  Proof.
+   intros; case (compare x y); intros H'; try (exfalso; order).
+   exists H'; auto.
+  Qed.
+
+  Lemma elim_compare_lt :
+   forall x y : t,
+   lt x y -> exists H : lt x y, compare x y = LT _ H.
+  Proof.
+   intros; case (compare x y); intros H'; try (exfalso; order).
+   exists H'; auto.
+  Qed.
+
+  Lemma elim_compare_gt :
+   forall x y : t,
+   lt y x -> exists H : lt y x, compare x y = GT _ H.
+  Proof.
+   intros; case (compare x y); intros H'; try (exfalso; order).
+   exists H'; auto.
+  Qed.
+
+  Ltac elim_comp :=
+    match goal with
+      | |- ?e => match e with
+           | context ctx [ compare ?a ?b ] =>
+                let H := fresh in
+                (destruct (compare a b) as [H|H|H]; try order)
+         end
+    end.
+
+  Ltac elim_comp_eq x y :=
+    elim (elim_compare_eq (x:=x) (y:=y));
+     [ intros _1 _2; rewrite _2; clear _1 _2 | auto ].
+
+  Ltac elim_comp_lt x y :=
+    elim (elim_compare_lt (x:=x) (y:=y));
+     [ intros _1 _2; rewrite _2; clear _1 _2 | auto ].
+
+  Ltac elim_comp_gt x y :=
+    elim (elim_compare_gt (x:=x) (y:=y));
+     [ intros _1 _2; rewrite _2; clear _1 _2 | auto ].
+
+  (** 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); [ left | right | right ]; auto.
+  Defined.
+
+  Definition eqb x y : bool := if eq_dec x y then true else false.
+
+  Lemma eqb_alt :
+    forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end.
+  Proof.
+  unfold eqb; intros; destruct (eq_dec x y); elim_comp; 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. exact (InA_eqA eq_equiv). 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.
+
+Module KeyOrderedType(O:OrderedType).
+ Import O.
+ Module MO:=OrderedTypeFacts(O).
+ Import MO.
+
+ 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').
+  Definition ltk (p p':key*elt) := lt (fst p) (fst p').
+
+  Hint Unfold eqk eqke ltk.
+  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.
+
+  (* ltk ignore the second components *)
+
+   Lemma ltk_right_r : forall x k e e', ltk x (k,e) -> ltk x (k,e').
+   Proof. auto. Qed.
+
+   Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
+   Proof. auto. Qed.
+   Hint Immediate ltk_right_r ltk_right_l.
+
+  (* eqk, eqke are equalities, ltk is a strict order *)
+
+  Lemma eqk_refl : forall e, eqk e e.
+  Proof. auto. Qed.
+
+  Lemma eqke_refl : forall e, eqke e e.
+  Proof. auto. Qed.
+
+  Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.
+  Proof. auto. Qed.
+
+  Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.
+  Proof. unfold eqke; intuition. Qed.
+
+  Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
+  Proof. eauto. Qed.
+
+  Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
+  Proof.
+    unfold eqke; intuition; [ eauto | congruence ].
+  Qed.
+
+  Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''.
+  Proof. eauto. Qed.
+
+  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
+  Proof. unfold eqk, ltk; auto. Qed.
+
+  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
+  Proof.
+    unfold eqke, ltk; intuition; simpl in *; subst.
+    exact (lt_not_eq H H1).
+  Qed.
+
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
+  Hint Immediate eqk_sym eqke_sym.
+
+  Global Instance eqk_equiv : Equivalence eqk.
+  Proof. split; eauto. Qed.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+  Proof. split; eauto. Qed.
+
+  Global Instance ltk_strorder : StrictOrder ltk.
+  Proof.
+   split; eauto.
+   intros (x,e); compute; apply (StrictOrder_Irreflexive x).
+  Qed.
+
+  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
+  Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
+  (* Additionnal facts *)
+
+  Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'.
+   Proof.
+     unfold eqk, ltk; simpl; auto.
+   Qed.
+
+  Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''.
+  Proof. eauto. Qed.
+
+  Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''.
+  Proof.
+      intros (k,e) (k',e') (k'',e'').
+      unfold ltk, eqk; simpl; eauto.
+  Qed.
+  Hint Resolve eqk_not_ltk.
+  Hint Immediate ltk_eqk eqk_ltk.
+
+  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.
+
+  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.
+  exists e; auto.
+  destruct IHInA as [e H0].
+  exists e; auto.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
+  Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof.
+  destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
+  Qed.
+
+  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
+  Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed.
+
+  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
+  Proof. exact (InfA_ltA ltk_strorder). 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.
+  exact (SortA_InfA_InA eqk_equiv ltk_strorder ltk_compat).
+  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.
+  exact (SortA_NoDupA eqk_equiv ltk_strorder ltk_compat).
+  Qed.
+
+  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
+  Proof.
+   inversion 1; intros; 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.
+    inversion_clear 2; 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.
+    inversion_clear 1; red; intros.
+    destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)).
+  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 Unfold eqk eqke ltk.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+ Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
+ Hint Immediate eqk_sym eqke_sym.
+ Hint Resolve eqk_not_ltk.
+ Hint Immediate ltk_eqk eqk_ltk.
+ 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.
+
+
diff --git a/theories/Structures/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v
new file mode 100644
index 00000000..23ae4c85
--- /dev/null
+++ b/theories/Structures/OrderedTypeAlt.v
@@ -0,0 +1,122 @@
+(***********************************************************************)
+(*  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$ *)
+
+Require Import OrderedType.
+
+(** * An alternative (but equivalent) presentation for an Ordered Type
+   inferface. *)
+
+(** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt]
+whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ]
+*)
+
+Module Type OrderedTypeAlt.
+
+ Parameter t : Type.
+
+ Parameter compare : t -> t -> comparison.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Parameter compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Parameter compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+
+End OrderedTypeAlt.
+
+(** From this new presentation to the original one. *)
+
+Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType.
+ Import O.
+
+ Definition t := t.
+
+ Definition eq x y := (x?=y) = Eq.
+ Definition lt x y := (x?=y) = Lt.
+
+ Lemma eq_refl : forall x, eq x x.
+ Proof.
+ intro x.
+ unfold eq.
+ assert (H:=compare_sym x x).
+ destruct (x ?= x); simpl in *; try discriminate; auto.
+ Qed.
+
+ Lemma eq_sym : forall x y, eq x y -> eq y x.
+ Proof.
+ unfold eq; intros.
+ rewrite compare_sym.
+ rewrite H; simpl; auto.
+ Qed.
+
+ Definition eq_trans := (compare_trans Eq).
+
+ Definition lt_trans := (compare_trans Lt).
+
+ Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
+ Proof.
+ unfold eq, lt; intros.
+ rewrite H; discriminate.
+ Qed.
+
+ Definition compare : forall x y, Compare lt eq x y.
+ Proof.
+ intros.
+ case_eq (x ?= y); intros.
+ apply EQ; auto.
+ apply LT; auto.
+ apply GT; red.
+ rewrite compare_sym; rewrite H; auto.
+ Defined.
+
+ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+ Proof.
+ intros; unfold eq.
+ case (x ?= y); [ left | right | right ]; auto; discriminate.
+ Defined.
+
+End OrderedType_from_Alt.
+
+(** From the original presentation to this alternative one. *)
+
+Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt.
+ Import O.
+ Module MO:=OrderedTypeFacts(O).
+ Import MO.
+
+ Definition t := t.
+
+ Definition compare x y := match compare x y with
+   | LT _ => Lt
+   | EQ _ => Eq
+   | GT _ => Gt
+  end.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Lemma compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Proof.
+ intros x y; unfold compare.
+ destruct O.compare; elim_comp; simpl; auto.
+ Qed.
+
+ Lemma compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+ Proof.
+ intros c x y z.
+ destruct c; unfold compare;
+ do 2 (destruct O.compare; intros; try discriminate);
+ elim_comp; auto.
+ Qed.
+
+End OrderedType_to_Alt.
+
+
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
new file mode 100644
index 00000000..b4dbceba
--- /dev/null
+++ b/theories/Structures/OrderedTypeEx.v
@@ -0,0 +1,333 @@
+(***********************************************************************)
+(*  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$ *)
+
+Require Import OrderedType.
+Require Import ZArith.
+Require Import Omega.
+Require Import NArith Ndec.
+Require Import Compare_dec.
+
+(** * Examples of Ordered Type structures. *)
+
+(** First, a particular case of [OrderedType] where
+    the equality is the usual one of Coq. *)
+
+Module Type UsualOrderedType.
+ Parameter Inline t : Type.
+ Definition eq := @eq t.
+ Parameter Inline lt : t -> t -> Prop.
+ Definition eq_refl := @refl_equal t.
+ Definition eq_sym := @sym_eq t.
+ Definition eq_trans := @trans_eq t.
+ Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+ Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+ Parameter compare : forall x y : t, Compare lt eq x y.
+ Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq 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 eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt := lt.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+  Proof. unfold lt; intros; apply lt_trans with y; auto. Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+  Proof. unfold lt, eq; intros; omega. Qed.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+    intros x y; destruct (nat_compare x y) as [ | | ]_eqn.
+    apply EQ. apply nat_compare_eq; assumption.
+    apply LT. apply nat_compare_Lt_lt; assumption.
+    apply GT. apply nat_compare_Gt_gt; assumption.
+  Defined.
+
+  Definition eq_dec := eq_nat_dec.
+
+End Nat_as_OT.
+
+
+(** [Z] is an ordered type with respect to the usual order on integers. *)
+
+Open Local Scope Z_scope.
+
+Module Z_as_OT <: UsualOrderedType.
+
+  Definition t := Z.
+  Definition eq := @eq Z.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt (x y:Z) := (x<y).
+
+  Lemma lt_trans : forall x y z, x<y -> y<z -> x<z.
+  Proof. intros; omega. Qed.
+
+  Lemma lt_not_eq : forall x y, x<y -> ~ x=y.
+  Proof. intros; omega. Qed.
+
+  Definition compare : forall x y, Compare lt eq x y.
+  Proof.
+    intros x y; destruct (x ?= y) as [ | | ]_eqn.
+    apply EQ; apply Zcompare_Eq_eq; assumption.
+    apply LT; assumption.
+    apply GT; apply Zgt_lt; assumption.
+  Defined.
+
+  Definition eq_dec := Z_eq_dec.
+
+End Z_as_OT.
+
+(** [positive] is an ordered type with respect to the usual order on natural numbers. *)
+
+Open Local Scope positive_scope.
+
+Module Positive_as_OT <: UsualOrderedType.
+  Definition t:=positive.
+  Definition eq:=@eq positive.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt p q:= (p ?= q) Eq = Lt.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+  Proof.
+  unfold lt; intros x y z.
+  change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z).
+  omega.
+  Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+  Proof.
+  intros; intro.
+  rewrite H0 in H.
+  unfold lt in H.
+  rewrite Pcompare_refl in H; discriminate.
+  Qed.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+  intros x y. destruct ((x ?= y) Eq) as [ | | ]_eqn.
+  apply EQ; apply Pcompare_Eq_eq; assumption.
+  apply LT; assumption.
+  apply GT; apply ZC1; assumption.
+  Defined.
+
+  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. *)
+
+Open Local Scope positive_scope.
+
+Module N_as_OT <: UsualOrderedType.
+  Definition t:=N.
+  Definition eq:=@eq N.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt:=Nlt.
+  Definition lt_trans := Nlt_trans.
+  Definition lt_not_eq := Nlt_not_eq.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+  intros x y. destruct (x ?= y)%N as [ | | ]_eqn.
+  apply EQ; apply Ncompare_Eq_eq; assumption.
+  apply LT; assumption.
+  apply GT. apply Ngt_Nlt; assumption.
+  Defined.
+
+  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.
+
+
+(** From two ordered types, we can build a new OrderedType
+   over their cartesian product, using the lexicographic order. *)
+
+Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
+ Module MO1:=OrderedTypeFacts(O1).
+ Module MO2:=OrderedTypeFacts(O2).
+
+ Definition t := prod O1.t O2.t.
+
+ Definition eq x y := O1.eq (fst x) (fst y) /\ O2.eq (snd x) (snd y).
+
+ Definition lt x y :=
+    O1.lt (fst x) (fst y) \/
+    (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)).
+
+ Lemma eq_refl : forall x : t, eq x x.
+ Proof.
+ intros (x1,x2); red; simpl; auto.
+ Qed.
+
+ Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+ Proof.
+ intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
+ Qed.
+
+ Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+ Proof.
+ intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto.
+ Qed.
+
+ Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+ Proof.
+ intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition.
+ left; eauto.
+ left; eapply MO1.lt_eq; eauto.
+ left; eapply MO1.eq_lt; eauto.
+ right; split; eauto.
+ Qed.
+
+ Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+ Proof.
+ intros (x1,x2) (y1,y2); unfold eq, lt; simpl; intuition.
+ apply (O1.lt_not_eq H0 H1).
+ apply (O2.lt_not_eq H3 H2).
+ Qed.
+
+ Definition compare : forall x y : t, Compare lt eq x y.
+ intros (x1,x2) (y1,y2).
+ destruct (O1.compare x1 y1).
+ apply LT; unfold lt; auto.
+ destruct (O2.compare x2 y2).
+ apply LT; unfold lt; auto.
+ apply EQ; unfold eq; auto.
+ apply GT; unfold lt; auto.
+ apply GT; unfold lt; auto.
+ Defined.
+
+ Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
+ Proof.
+ intros; elim (compare x y); intro H; [ right | left | right ]; auto.
+ auto using lt_not_eq.
+ assert (~ eq y x); auto using lt_not_eq, eq_sym.
+ Defined.
+
+End PairOrderedType.
+
+
+(** Even if [positive] can be seen as an ordered type with respect to the
+  usual order (see above), we can also use a lexicographic order over bits
+  (lower bits are considered first). This is more natural when using
+  [positive] as indexes for sets or maps (see FSetPositive and FMapPositive. *)
+
+Module PositiveOrderedTypeBits <: UsualOrderedType.
+  Definition t:=positive.
+  Definition eq:=@eq positive.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Fixpoint bits_lt (p q:positive) : Prop :=
+   match p, q with
+   | xH, xI _ => True
+   | xH, _ => False
+   | xO p, xO q => bits_lt p q
+   | xO _, _ => True
+   | xI p, xI q => bits_lt p q
+   | xI _, _ => False
+   end.
+
+  Definition lt:=bits_lt.
+
+  Lemma bits_lt_trans :
+    forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
+  Proof.
+  induction x.
+  induction y; destruct z; simpl; eauto; intuition.
+  induction y; destruct z; simpl; eauto; intuition.
+  induction y; destruct z; simpl; eauto; intuition.
+  Qed.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+  Proof.
+  exact bits_lt_trans.
+  Qed.
+
+  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
+  Proof.
+  induction x; simpl; auto.
+  Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+  Proof.
+  intros; intro.
+  rewrite <- H0 in H; clear H0 y.
+  unfold lt in H.
+  exact (bits_lt_antirefl x H).
+  Qed.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+  induction x; destruct y.
+  (* I I *)
+  destruct (IHx y).
+  apply LT; auto.
+  apply EQ; rewrite e; red; auto.
+  apply GT; auto.
+  (* I O *)
+  apply GT; simpl; auto.
+  (* I H *)
+  apply GT; simpl; auto.
+  (* O I *)
+  apply LT; simpl; auto.
+  (* O O *)
+  destruct (IHx y).
+  apply LT; auto.
+  apply EQ; rewrite e; red; auto.
+  apply GT; auto.
+  (* O H *)
+  apply LT; simpl; auto.
+  (* H I *)
+  apply LT; simpl; auto.
+  (* H O *)
+  apply GT; simpl; auto.
+  (* H H *)
+  apply EQ; red; auto.
+  Qed.
+
+  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
+  Proof.
+  intros. case_eq ((x ?= y) Eq); intros.
+  left. apply Pcompare_Eq_eq; auto.
+  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
+  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
+  Qed.
+
+End PositiveOrderedTypeBits.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
new file mode 100644
index 00000000..bddd461a
--- /dev/null
+++ b/theories/Structures/Orders.v
@@ -0,0 +1,333 @@
+(***********************************************************************)
+(*  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$ *)
+
+Require Export Relations Morphisms Setoid Equalities.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Ordered types *)
+
+(** First, signatures with only the order relations *)
+
+Module Type HasLt (Import T:Typ).
+  Parameter Inline lt : t -> t -> Prop.
+End HasLt.
+
+Module Type HasLe (Import T:Typ).
+  Parameter Inline le : t -> t -> Prop.
+End HasLe.
+
+Module Type EqLt := Typ <+ HasEq <+ HasLt.
+Module Type EqLe := Typ <+ HasEq <+ HasLe.
+Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe.
+
+(** Versions with nice notations *)
+
+Module Type LtNotation (E:EqLt).
+  Infix "<" := E.lt.
+  Notation "x > y" := (y<x) (only parsing).
+  Notation "x < y < z" := (x<y /\ y<z).
+End LtNotation.
+
+Module Type LeNotation (E:EqLe).
+  Infix "<=" := E.le.
+  Notation "x >= y" := (y<=x) (only parsing).
+  Notation "x <= y <= z" := (x<=y /\ y<=z).
+End LeNotation.
+
+Module Type LtLeNotation (E:EqLtLe).
+  Include LtNotation E <+ LeNotation E.
+  Notation "x <= y < z" := (x<=y /\ y<z).
+  Notation "x < y <= z" := (x<y /\ y<=z).
+End LtLeNotation.
+
+Module Type EqLtNotation (E:EqLt) := EqNotation E <+ LtNotation E.
+Module Type EqLeNotation (E:EqLe) := EqNotation E <+ LeNotation E.
+Module Type EqLtLeNotation (E:EqLtLe) := EqNotation E <+ LtLeNotation E.
+
+Module Type EqLt' := EqLt <+ EqLtNotation.
+Module Type EqLe' := EqLe <+ EqLeNotation.
+Module Type EqLtLe' := EqLtLe <+ EqLtLeNotation.
+
+(** Versions with logical specifications *)
+
+Module Type IsStrOrder (Import E:EqLt).
+  Declare Instance lt_strorder : StrictOrder lt.
+  Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
+End IsStrOrder.
+
+Module Type LeIsLtEq (Import E:EqLtLe').
+  Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
+End LeIsLtEq.
+
+Module Type HasCompare (Import E:EqLt).
+  Parameter Inline compare : t -> t -> comparison.
+  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+End HasCompare.
+
+Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
+Module Type DecStrOrder := StrOrder <+ HasCompare.
+Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
+Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
+
+Module Type StrOrder' := StrOrder <+ EqLtNotation.
+Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
+Module Type OrderedType' := OrderedType <+ EqLtNotation.
+Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.
+
+(** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
+  But adding this redundant field allows to see an [OrderedType] as a
+  [DecidableType]. *)
+
+(** * Versions with [eq] being the usual Leibniz equality of Coq *)
+
+Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder.
+Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare.
+Module Type UsualOrderedType <: UsualDecidableType <: OrderedType
+ := UsualDecStrOrder <+ HasEqDec.
+Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq.
+
+(** NB: in [UsualOrderedType], the field [lt_compat] is
+    useless since [eq] is [Leibniz], but it should be
+    there for subtyping. *)
+
+Module Type UsualStrOrder' := UsualStrOrder <+ LtNotation.
+Module Type UsualDecStrOrder' := UsualDecStrOrder <+ LtNotation.
+Module Type UsualOrderedType' := UsualOrderedType <+ LtNotation.
+Module Type UsualOrderedTypeFull' := UsualOrderedTypeFull <+ LtLeNotation.
+
+(** * Purely logical versions *)
+
+Module Type LtIsTotal (Import E:EqLt').
+  Axiom lt_total : forall x y, x<y \/ x==y \/ y<x.
+End LtIsTotal.
+
+Module Type TotalOrder := StrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
+Module Type UsualTotalOrder <: TotalOrder
+ := UsualStrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
+
+Module Type TotalOrder' := TotalOrder <+ EqLtLeNotation.
+Module Type UsualTotalOrder' := UsualTotalOrder <+ LtLeNotation.
+
+(** * Conversions *)
+
+(** From [compare] to [eqb], and then [eq_dec] *)
+
+Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O.
+
+ Definition eqb x y :=
+   match compare x y with Eq => true | _ => false end.
+
+ Lemma eqb_eq : forall x y, eqb x y = true <-> x==y.
+ Proof.
+ unfold eqb. intros x y.
+ destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate.
+ intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ Qed.
+
+End Compare2EqBool.
+
+Module DSO_to_OT (O:DecStrOrder) <: OrderedType :=
+  O <+ Compare2EqBool <+ HasEqBool2Dec.
+
+(** From [OrderedType] To [OrderedTypeFull] (adding [<=]) *)
+
+Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
+ Include O.
+ Definition le x y := x<y \/ x==y.
+ Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y.
+ Proof. unfold le; split; auto. Qed.
+End OT_to_Full.
+
+(** From computational to logical versions *)
+
+Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O.
+ Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+ Proof. intros; destruct (compare_spec x y); auto. Qed.
+End OTF_LtIsTotal.
+
+Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
+ := O <+ OTF_LtIsTotal.
+
+
+(** * Versions with boolean comparisons
+
+    This style is used in [Mergesort]
+*)
+
+(** For stating properties like transitivity  of [leb],
+    we coerce [bool] into [Prop]. *)
+
+Local Coercion is_true : bool >-> Sortclass.
+Hint Unfold is_true.
+
+Module Type HasLeBool (Import T:Typ).
+  Parameter Inline leb : t -> t -> bool.
+End HasLeBool.
+
+Module Type HasLtBool (Import T:Typ).
+  Parameter Inline ltb : t -> t -> bool.
+End HasLtBool.
+
+Module Type LeBool := Typ <+ HasLeBool.
+Module Type LtBool := Typ <+ HasLtBool.
+
+Module Type LeBoolNotation (E:LeBool).
+  Infix "<=?" := E.leb (at level 35).
+End LeBoolNotation.
+
+Module Type LtBoolNotation (E:LtBool).
+  Infix "<?" := E.ltb (at level 35).
+End LtBoolNotation.
+
+Module Type LeBool' := LeBool <+ LeBoolNotation.
+Module Type LtBool' := LtBool <+ LtBoolNotation.
+
+Module Type LeBool_Le (T:Typ)(X:HasLeBool T)(Y:HasLe T).
+ Parameter leb_le : forall x y, X.leb x y = true <-> Y.le x y.
+End LeBool_Le.
+
+Module Type LtBool_Lt (T:Typ)(X:HasLtBool T)(Y:HasLt T).
+ Parameter ltb_lt : forall x y, X.ltb x y = true <-> Y.lt x y.
+End LtBool_Lt.
+
+Module Type LeBoolIsTotal (Import X:LeBool').
+ Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true.
+End LeBoolIsTotal.
+
+Module Type TotalLeBool := LeBool <+ LeBoolIsTotal.
+Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal.
+
+Module Type LeBoolIsTransitive (Import X:LeBool').
+ Axiom leb_trans : Transitive X.leb.
+End LeBoolIsTransitive.
+
+Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive.
+Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive.
+
+
+(** * From [OrderedTypeFull] to [TotalTransitiveLeBool] *)
+
+Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.
+
+ Definition leb x y :=
+  match compare x y with Gt => false | _ => true end.
+
+ Lemma leb_le : forall x y, leb x y <-> x <= y.
+ Proof.
+ intros. unfold leb. rewrite le_lteq.
+ destruct (compare_spec x y) as [EQ|LT|GT]; split; auto.
+ discriminate.
+ intros LE. elim (StrictOrder_Irreflexive x).
+ destruct LE as [LT|EQ]. now transitivity y. now rewrite <- EQ in GT.
+ Qed.
+
+ Lemma leb_total : forall x y, leb x y \/ leb y x.
+ Proof.
+ intros. rewrite 2 leb_le. rewrite 2 le_lteq.
+ destruct (compare_spec x y); intuition.
+ Qed.
+
+ Lemma leb_trans : Transitive leb.
+ Proof.
+ intros x y z. rewrite !leb_le, !le_lteq.
+ intros [Hxy|Hxy] [Hyz|Hyz].
+ left; transitivity y; auto.
+ left; rewrite <- Hyz; auto.
+ left; rewrite Hxy; auto.
+ right; transitivity y; auto.
+ Qed.
+
+ Definition t := t.
+
+End OTF_to_TTLB.
+
+
+(** * From [TotalTransitiveLeBool] to [OrderedTypeFull]
+
+    [le] is [leb ... = true].
+    [eq] is [le /\ swap le].
+    [lt] is [le /\ ~swap le].
+*)
+
+Local Open Scope bool_scope.
+
+Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
+
+ Definition t := t.
+
+ Definition le x y : Prop := x <=? y.
+ Definition eq x y : Prop := le x y /\ le y x.
+ Definition lt x y : Prop := le x y /\ ~le y x.
+
+ Definition compare x y :=
+  if x <=? y then (if y <=? x then Eq else Lt) else Gt.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+ intros. unfold compare.
+ case_eq (x <=? y).
+ case_eq (y <=? x).
+ constructor. split; auto.
+ constructor. split; congruence.
+ constructor. destruct (leb_total x y); split; congruence.
+ Qed.
+
+ Definition eqb x y := (x <=? y) && (y <=? x).
+
+ Lemma eqb_eq : forall x y, eqb x y <-> eq x y.
+ Proof.
+ intros. unfold eq, eqb, le.
+ case leb; simpl; intuition; discriminate.
+ Qed.
+
+ Include HasEqBool2Dec.
+
+ Instance eq_equiv : Equivalence eq.
+ Proof.
+ split.
+ intros x; unfold eq, le. destruct (leb_total x x); auto.
+ intros x y; unfold eq, le. intuition.
+ intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto.
+ Qed.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+ split.
+ intros x. unfold lt; red; intuition.
+ intros x y z; unfold lt, le. intuition.
+ apply leb_trans with y; auto.
+ absurd (z <=? y); auto.
+ apply leb_trans with x; auto.
+ Qed.
+
+ Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
+ Proof.
+ apply proper_sym_impl_iff_2; auto with *.
+ intros x x' Hx y y' Hy' H. unfold eq, lt, le in *.
+ intuition.
+ apply leb_trans with x; auto.
+ apply leb_trans with y; auto.
+ absurd (y <=? x); auto.
+ apply leb_trans with x'; auto.
+ apply leb_trans with y'; auto.
+ Qed.
+
+ Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+ Proof.
+ intros.
+ unfold lt, eq, le.
+ split; [ | intuition ].
+ intros LE.
+ case_eq (y <=? x); [right|left]; intuition; try discriminate.
+ Qed.
+
+End TTLB_to_OTF.
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v
new file mode 100644
index 00000000..d86b02a1
--- /dev/null
+++ b/theories/Structures/OrdersAlt.v
@@ -0,0 +1,242 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* Finite sets library.
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id$ *)
+
+Require Import OrderedType Orders.
+Set Implicit Arguments.
+
+(** * Some alternative (but equivalent) presentations for an Ordered Type
+   inferface. *)
+
+(** ** The original interface *)
+
+Module Type OrderedTypeOrig := OrderedType.OrderedType.
+
+(** ** An interface based on compare *)
+
+Module Type OrderedTypeAlt.
+
+ Parameter t : Type.
+
+ Parameter compare : t -> t -> comparison.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Parameter compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Parameter compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+
+End OrderedTypeAlt.
+
+(** ** From OrderedTypeOrig to OrderedType. *)
+
+Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
+
+ Include Update_DT O.  (* Provides : t eq eq_equiv eq_dec *)
+
+ Definition lt := O.lt.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+  split.
+  intros x Hx. apply (O.lt_not_eq Hx); auto with *.
+  exact O.lt_trans.
+ Qed.
+
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof.
+  apply proper_sym_impl_iff_2; auto with *.
+  intros x x' Hx y y' Hy H.
+  assert (H0 : lt x' y).
+   destruct (O.compare x' y) as [H'|H'|H']; auto.
+   elim (O.lt_not_eq H). transitivity x'; auto with *.
+   elim (O.lt_not_eq (O.lt_trans H H')); auto.
+  destruct (O.compare x' y') as [H'|H'|H']; auto.
+  elim (O.lt_not_eq H).
+   transitivity x'; auto with *. transitivity y'; auto with *.
+  elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *.
+ Qed.
+
+ Definition compare x y :=
+   match O.compare x y with
+    | EQ _ => Eq
+    | LT _ => Lt
+    | GT _ => Gt
+  end.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+  intros; unfold compare; destruct O.compare; auto.
+ Qed.
+
+End Update_OT.
+
+(** ** From OrderedType to OrderedTypeOrig. *)
+
+Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.
+
+ Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *)
+
+ Definition lt := O.lt.
+
+ Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
+ Proof.
+  intros x y L E; rewrite E in L. apply (StrictOrder_Irreflexive y); auto.
+ Qed.
+
+ Lemma lt_trans : Transitive lt.
+ Proof. apply O.lt_strorder. Qed.
+
+ Definition compare : forall x y, Compare lt eq x y.
+ Proof.
+  intros x y; destruct (CompSpec2Type (O.compare_spec x y));
+   [apply EQ|apply LT|apply GT]; auto.
+ Defined.
+
+End Backport_OT.
+
+
+(** ** From OrderedTypeAlt to OrderedType. *)
+
+Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
+
+ Definition t := t.
+
+ Definition eq x y := (x?=y) = Eq.
+ Definition lt x y := (x?=y) = Lt.
+
+ Instance eq_equiv : Equivalence eq.
+ Proof.
+  split; red.
+  (* refl *)
+  unfold eq; intros x.
+  assert (H:=compare_sym x x).
+  destruct (x ?= x); simpl in *; auto; discriminate.
+  (* sym *)
+  unfold eq; intros x y H.
+  rewrite compare_sym, H; simpl; auto.
+  (* trans *)
+  apply compare_trans.
+ Qed.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+  split; repeat red; unfold lt; try apply compare_trans.
+  intros x H.
+  assert (eq x x) by reflexivity.
+  unfold eq in *; congruence.
+ Qed.
+
+ Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
+ Proof.
+  unfold lt, eq; intros x y z Hxy Hyz.
+  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
+  rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
+  rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
+  rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
+ Qed.
+
+ Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
+ Proof.
+  unfold lt, eq; intros x y z Hxy Hyz.
+  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
+  rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
+  rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
+  rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
+ Qed.
+
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof.
+  apply proper_sym_impl_iff_2; auto with *.
+  repeat red; intros.
+  eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto.
+ Qed.
+
+ Definition compare := O.compare.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+  unfold eq, lt, compare; intros.
+  destruct (O.compare x y) as [ ]_eqn:H; auto.
+  apply CompGt.
+  rewrite compare_sym, H; auto.
+ Qed.
+
+ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+ Proof.
+ intros; unfold eq.
+ case (x ?= y); [ left | right | right ]; auto; discriminate.
+ Defined.
+
+End OT_from_Alt.
+
+(** From the original presentation to this alternative one. *)
+
+Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
+
+ Definition t := t.
+ Definition compare := compare.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Lemma compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Proof.
+ intros x y; unfold compare.
+ 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.
+ rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
+ rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
+ rewrite V in U. elim (StrictOrder_Irreflexive y); auto.
+ Qed.
+
+ Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y.
+ Proof.
+ unfold compare.
+ 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.
+
+ Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y.
+ Proof.
+ unfold compare.
+ 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.
+
+ Lemma compare_Gt : forall x y, compare x y = Gt <-> lt y x.
+ Proof.
+ intros x y. rewrite compare_sym, CompOpp_iff. apply compare_Lt.
+ Qed.
+
+ Lemma compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+ Proof.
+ intros c x y z.
+ destruct c; unfold compare;
+  rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt;
+  transitivity y; auto.
+ Qed.
+
+End OT_to_Alt.
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
new file mode 100644
index 00000000..56f1d5de
--- /dev/null
+++ b/theories/Structures/OrdersEx.v
@@ -0,0 +1,88 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* Finite sets library.
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id$ *)
+
+Require Import Orders NatOrderedType POrderedType NOrderedType
+ ZOrderedType RelationPairs EqualitiesFacts.
+
+(** * Examples of Ordered Type structures. *)
+
+
+(** 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 *)
+
+Module OT_as_DT (O:OrderedType) <: DecidableType := O.
+
+(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *)
+
+Module Nat_as_DT <: UsualDecidableType := Nat_as_OT.
+Module Positive_as_DT <: UsualDecidableType := Positive_as_OT.
+Module N_as_DT <: UsualDecidableType := N_as_OT.
+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 lt :=
+   (relation_disjunction (O1.lt @@1) (O1.eq * O2.lt))%signature.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+ split.
+ (* irreflexive *)
+ intros (x1,x2); compute. destruct 1.
+ apply (StrictOrder_Irreflexive x1); auto.
+ apply (StrictOrder_Irreflexive x2); intuition.
+ (* transitive *)
+ intros (x1,x2) (y1,y2) (z1,z2). compute. intuition.
+ left; etransitivity; eauto.
+ left. setoid_replace z1 with y1; auto with relations.
+ left; setoid_replace x1 with y1; auto with relations.
+ right; split; etransitivity; eauto.
+ Qed.
+
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof.
+ compute.
+ intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2).
+ rewrite X1,X2,Y1,Y2; intuition.
+ Qed.
+
+ Definition compare x y :=
+  match O1.compare (fst x) (fst y) with
+   | Eq => O2.compare (snd x) (snd y)
+   | Lt => Lt
+   | Gt => Gt
+  end.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+ 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 with relations.
+ Qed.
+
+End PairOrderedType.
+
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
new file mode 100644
index 00000000..a28b7977
--- /dev/null
+++ b/theories/Structures/OrdersFacts.v
@@ -0,0 +1,234 @@
+(***********************************************************************)
+(*  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 OrdersTac.
+Require Export Orders.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Properties of [OrderedTypeFull] *)
+
+Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
+
+ Module OrderTac := OTF_to_OrderTac O.
+ Ltac order := OrderTac.order.
+ Ltac iorder := intuition order.
+
+ Instance le_compat : Proper (eq==>eq==>iff) le.
+ Proof. repeat red; iorder. Qed.
+
+ Instance le_preorder : PreOrder le.
+ Proof. split; red; order. Qed.
+
+ Instance le_order : PartialOrder eq le.
+ Proof. compute; iorder. Qed.
+
+ Instance le_antisym : Antisymmetric _ eq le.
+ Proof. apply partial_order_antisym; auto with *. Qed.
+
+ Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
+ Proof. iorder. Qed.
+
+ Lemma lt_not_ge_iff : forall x y, x<y <-> ~y<=x.
+ Proof. iorder. Qed.
+
+ Lemma le_or_gt : forall x y, x<=y \/ y<x.
+ Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
+
+ Lemma lt_or_ge : forall x y, x<y \/ y<=x.
+ Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
+
+ Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
+ Proof. iorder. Qed.
+
+End OrderedTypeFullFacts.
+
+
+(** * Properties of [OrderedType] *)
+
+Module OrderedTypeFacts (Import O: OrderedType').
+
+  Module OrderTac := OT_to_OrderTac O.
+  Ltac order := OrderTac.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; simpl; 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 x y; destruct (CompSpec2Type (compare_spec 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.
+
+End OrderedTypeFacts.
+
+
+
+
+
+
+(** * Tests of the order tactic
+
+    Is it at least capable of proving some basic properties ? *)
+
+Module OrderedTypeTest (Import 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, CompSpec eq lt x y (compare x y).
+Proof.
+intros; unfold compare, eq, lt, flip.
+destruct (O.compare_spec y x); auto with relations.
+Qed.
+
+End OrderedTypeRev.
+
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
new file mode 100644
index 00000000..2ed07026
--- /dev/null
+++ b/theories/Structures/OrdersLists.v
@@ -0,0 +1,256 @@
+(***********************************************************************)
+(*  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 Orders.
+
+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 @@1.
+  Definition eqke : relation (key*elt) := eq * Logic.eq.
+  Definition ltk : relation (key*elt) := lt @@1.
+
+  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.
+    repeat red; reflexivity.
+  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 with relations.
+    left; apply Sort_In_cons_1 with l; auto with relations.
+  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 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.
+
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
new file mode 100644
index 00000000..66a672c9
--- /dev/null
+++ b/theories/Structures/OrdersTac.v
@@ -0,0 +1,293 @@
+(***********************************************************************)
+(*  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 Setoid Morphisms Basics Equalities Orders.
+Set Implicit Arguments.
+
+(** * The order tactic *)
+
+(** This tactic is designed to solve systems of (in)equations
+    involving [eq], [lt], [le] and [~eq] on some type. This tactic is
+    domain-agnostic; it will only use equivalence+order axioms, and
+    not analyze elements of the domain. Hypothesis or goal of the form
+    [~lt] or [~le] are initially turned into [le] and [lt], other
+    parts of the goal are ignored. This initial preparation of the
+    goal is the only moment where totality is used. In particular,
+    the core of the tactic only proceeds by saturation of transitivity
+    and similar properties, and does not perform case splitting.
+    The tactic will fail if it doesn't solve the goal. *)
+
+
+(** An abstract vision of the predicates. This allows a one-line
+    statement for interesting transitivity properties: for instance
+    [trans_ord OLE OLE = OLE] will imply later
+    [le x y -> le y z -> le x z].
+*)
+
+Inductive ord := OEQ | OLT | OLE.
+Definition trans_ord o o' :=
+ match o, o' with
+ | OEQ, _ => o'
+ | _, OEQ => o
+ | OLE, OLE => OLE
+ | _, _ => OLT
+ end.
+Local Infix "+" := trans_ord.
+
+
+(** ** The requirements of the tactic : [TotalOrder].
+
+   [TotalOrder] contains an equivalence [eq],
+   a strict order [lt] total and compatible with [eq], and
+   a larger order [le] synonym for [lt\/eq].
+*)
+
+(** ** Properties that will be used by the [order] tactic *)
+
+Module OrderFacts(Import O:TotalOrder').
+
+(** Reflexivity rules *)
+
+Lemma eq_refl : forall x, x==x.
+Proof. reflexivity. Qed.
+
+Lemma le_refl : forall x, x<=x.
+Proof. intros; rewrite le_lteq; right; reflexivity. Qed.
+
+Lemma lt_irrefl : forall x, ~ x<x.
+Proof. intros; apply StrictOrder_Irreflexive. Qed.
+
+(** Symmetry rules *)
+
+Lemma eq_sym : forall x y, x==y -> y==x.
+Proof. auto with *. Qed.
+
+Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
+Proof.
+ intros x y; rewrite 2 le_lteq. intuition.
+ elim (StrictOrder_Irreflexive x); transitivity y; auto.
+Qed.
+
+Lemma neq_sym : forall x y, ~x==y -> ~y==x.
+Proof. auto using eq_sym. Qed.
+
+(** Transitivity rules : first, a generic formulation, then instances*)
+
+Ltac subst_eqns :=
+ match goal with
+   | H : _==_ |- _ => (rewrite H || rewrite <- H); clear H; subst_eqns
+   | _ => idtac
+ end.
+
+Definition interp_ord o :=
+ match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end.
+Local Notation "#" := interp_ord.
+
+Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
+Proof.
+destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition;
+ subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
+Qed.
+
+Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.
+Definition le_trans x y z : x<=y -> y<=z -> x<=z := @trans OLE OLE x y z.
+Definition lt_trans x y z : x<y -> y<z -> x<z := @trans OLT OLT x y z.
+Definition le_lt_trans x y z : x<=y -> y<z -> x<z := @trans OLE OLT x y z.
+Definition lt_le_trans x y z : x<y -> y<=z -> x<z := @trans OLT OLE x y z.
+Definition eq_lt x y z : x==y -> y<z -> x<z := @trans OEQ OLT x y z.
+Definition lt_eq x y z : x<y -> y==z -> x<z := @trans OLT OEQ x y z.
+Definition eq_le x y z : x==y -> y<=z -> x<=z := @trans OEQ OLE x y z.
+Definition le_eq x y z : x<=y -> y==z -> x<=z := @trans OLE OEQ x y z.
+
+Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z.
+Proof. eauto using eq_trans, eq_sym. Qed.
+
+Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z.
+Proof. eauto using eq_trans, eq_sym. Qed.
+
+(** (double) negation rules *)
+
+Lemma not_neq_eq : forall x y, ~~x==y -> x==y.
+Proof.
+intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto;
+ destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto.
+Qed.
+
+Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
+Proof.
+intros x y H. destruct (lt_total x y); auto.
+destruct H. rewrite le_lteq. intuition.
+Qed.
+
+Lemma not_gt_le : forall x y, ~y<x -> x<=y.
+Proof.
+intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition.
+Qed.
+
+Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y.
+Proof. auto using not_ge_lt, le_antisym. Qed.
+
+End OrderFacts.
+
+
+
+(** ** [MakeOrderTac] : The functor providing the order tactic. *)
+
+Module MakeOrderTac (Import O:TotalOrder').
+
+Include OrderFacts O.
+
+(** order_eq : replace x by y in all (in)equations hyps thanks
+   to equality EQ (where eq has been hidden in order to avoid
+   self-rewriting), then discard EQ. *)
+
+Ltac order_rewr x eqn :=
+ (* NB: we could use the real rewrite here, but proofs would be uglier. *)
+ let rewr H t := generalize t; clear H; intro H
+ in
+ match goal with
+ | H : x == _ |- _ => rewr H (eq_trans (eq_sym eqn) H); order_rewr x eqn
+ | H : _ == x |- _ => rewr H (eq_trans H eqn); order_rewr x eqn
+ | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym eqn) H); order_rewr x eqn
+ | H : ~_ == x |- _ => rewr H (neq_eq H eqn); order_rewr x eqn
+ | H : x < _ |- _ => rewr H (eq_lt (eq_sym eqn) H); order_rewr x eqn
+ | H : _ < x |- _ => rewr H (lt_eq H eqn); order_rewr x eqn
+ | H : x <= _ |- _ => rewr H (eq_le (eq_sym eqn) H); order_rewr x eqn
+ | H : _ <= x |- _ => rewr H (le_eq H eqn); order_rewr x eqn
+ | _ => clear eqn
+end.
+
+Ltac order_eq x y eqn :=
+ match x with
+ | y => clear eqn
+ | _ => change (interp_ord OEQ x y) in eqn; order_rewr x eqn
+ end.
+
+(** Goal preparation : We turn all negative hyps into positive ones
+  and try to prove False from the inverse of the current goal.
+  These steps require totality of our order. After this preparation,
+  order only deals with the context, and tries to prove False.
+  Hypotheses of the form [A -> False] are also folded in [~A]
+  for convenience (i.e. cope with the mess left by intuition). *)
+
+Ltac order_prepare :=
+ match goal with
+ | H : ?A -> False |- _ => change (~A) in H; order_prepare
+ | H : ~(?R ?x ?y) |- _ =>
+   match R with
+   | eq => fail 1 (* if already using [eq], we leave it this ways *)
+   | _ => (change (~x==y) in H ||
+           apply not_gt_le in H ||
+           apply not_ge_lt in H ||
+           clear H || fail 1); order_prepare
+   end
+ | H : ?R ?x ?y |- _ =>
+   match R with
+   | eq => fail 1
+   | lt => fail 1
+   | le => fail 1
+   | _ => (change (x==y) in H ||
+           change (x<y) in H ||
+           change (x<=y) in H ||
+           clear H || fail 1); order_prepare
+   end
+ | |- ~ _ => intro; order_prepare
+ | |- _ ?x ?x =>
+   exact (eq_refl x) || exact (le_refl x) || exfalso
+ | _ =>
+   (apply not_neq_eq; intro) ||
+   (apply not_ge_lt; intro) ||
+   (apply not_gt_le; intro) || exfalso
+ end.
+
+(** We now try to prove False from the various [< <= == !=] hypothesis *)
+
+Ltac order_loop :=
+ match goal with
+ (* First, successful situations *)
+ | H : ?x < ?x |- _ => exact (lt_irrefl H)
+ | H : ~ ?x == ?x |- _ => exact (H (eq_refl x))
+ (* Second, useless hyps *)
+ | H : ?x <= ?x |- _ => clear H; order_loop
+ (* Third, we eliminate equalities *)
+ | H : ?x == ?y |- _ => order_eq x y H; order_loop
+ (* Simultaneous le and ge is eq *)
+ | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ =>
+     generalize (le_antisym H1 H2); clear H1 H2; intro; order_loop
+ (* Simultaneous le and ~eq is lt *)
+ | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ =>
+     generalize (le_neq_lt H1 H2); clear H1 H2; intro; order_loop
+ | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ =>
+     generalize (le_neq_lt H1 (neq_sym H2)); clear H1 H2; intro; order_loop
+ (* Transitivity of lt and le *)
+ | H1 : ?x < ?y, H2 : ?y < ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (lt_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x <= ?y, H2 : ?y < ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (le_lt_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x < ?y, H2 : ?y <= ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (lt_le_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ =>
+    match goal with
+      | H : x <= z |- _ => fail 1
+      | _ => generalize (le_trans H1 H2); intro; order_loop
+    end
+ | _ => idtac
+end.
+
+(** The complete tactic. *)
+
+Ltac order :=
+ intros; order_prepare; order_loop; fail "Order tactic unsuccessful".
+
+End MakeOrderTac.
+
+Module OTF_to_OrderTac (OTF:OrderedTypeFull).
+ Module TO := OTF_to_TotalOrder OTF.
+ Include !MakeOrderTac TO.
+End OTF_to_OrderTac.
+
+Module OT_to_OrderTac (OT:OrderedType).
+ Module OTF := OT_to_Full OT.
+ Include !OTF_to_OrderTac OTF.
+End OT_to_OrderTac.
+
+Module TotalOrderRev (O:TotalOrder) <: TotalOrder.
+
+Definition t := O.t.
+Definition eq := O.eq.
+Definition lt := flip O.lt.
+Definition le := flip O.le.
+Include EqLtLeNotation.
+
+(* No Instance syntax to avoid saturating the Equivalence tables *)
+Definition eq_equiv := O.eq_equiv.
+
+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, x<=y <-> x<y \/ x==y.
+Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
+
+Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+Proof.
+ intros x y; unfold lt, eq, flip.
+ generalize (O.lt_total x y); intuition.
+Qed.
+
+End TotalOrderRev.
diff --git a/theories/Structures/vo.itarget b/theories/Structures/vo.itarget
new file mode 100644
index 00000000..674e9fba
--- /dev/null
+++ b/theories/Structures/vo.itarget
@@ -0,0 +1,14 @@
+Equalities.vo
+EqualitiesFacts.vo
+Orders.vo
+OrdersEx.vo
+OrdersFacts.vo
+OrdersLists.vo
+OrdersTac.vo
+OrdersAlt.vo
+GenericMinMax.vo
+DecidableType.vo
+DecidableTypeEx.vo
+OrderedTypeAlt.vo
+OrderedTypeEx.vo
+OrderedType.vo