OrderedType implementation for various numerical datatypes + min/max structures

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

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

5 files changed, 76 insertions, 126 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 70be28f87..408461a25 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -570,7 +570,7 @@ Fixpoint isok s :=
 (** * Correctness proofs *)
 
 (* Module Proofs. *)
- Module MX := OrderedTypeFacts X.
+ Module Import MX := OrderedTypeFacts X.
  Hint Resolve MX.lt_trans.
 
 (** * Automation and dedicated tactics *)
@@ -631,7 +631,7 @@ Lemma ltb_tree_iff : forall x s, lt_tree x s <-> ltb_tree x s = true.
 Proof.
  induction s as [|l IHl y r IHr h]; simpl.
  unfold lt_tree; intuition_in.
- MX.elim_compare x y; intros.
+ elim_compare x y.
  split; intros; try discriminate. assert (X.lt y x) by auto. order.
  split; intros; try discriminate. assert (X.lt y x) by auto. order.
  rewrite !andb_true_iff, <-IHl, <-IHr.
@@ -642,7 +642,7 @@ Lemma gtb_tree_iff : forall x s, gt_tree x s <-> gtb_tree x s = true.
 Proof.
  induction s as [|l IHl y r IHr h]; simpl.
  unfold gt_tree; intuition_in.
- MX.elim_compare x y; intros.
+ elim_compare x y.
  split; intros; try discriminate. assert (X.lt x y) by auto. order.
  rewrite !andb_true_iff, <-IHl, <-IHr.
   unfold gt_tree; intuition_in; order.
@@ -753,7 +753,7 @@ Functional Scheme union_ind := Induction for union Sort Prop.
 
 Ltac induct s x :=
  induction s as [|l IHl x' r IHr h]; simpl; intros;
- [|MX.elim_compare x x'; intros; inv].
+ [|elim_compare x x'; intros; inv].
 
 
 (** * Notations and helper lemma about pairs and triples *)
@@ -794,7 +794,7 @@ Qed.
 Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.
 Proof.
  split.
- induct s x; auto; discriminate.
+ induct s x; auto; try discriminate.
  induct s x; intuition_in; order.
 Qed.
 
@@ -1098,7 +1098,7 @@ Proof.
  assert (~X.lt x' x).
   apply min_elt_spec2 with s; auto.
   rewrite H; auto using min_elt_spec1.
- MX.elim_compare x x'; intuition.
+ elim_compare x x'; intuition.
 Qed.
 
 
@@ -1274,7 +1274,7 @@ Proof.
  intuition_in.
  factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv.
  rewrite join_spec, IHt0, IHt1, split_spec1, split_spec2; auto with *.
- MX.elim_compare y x1; intuition_in.
+ elim_compare y x1; intuition_in.
 Qed.
 
 Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2).
@@ -1316,7 +1316,8 @@ Proof.
  apply Hl; auto.
  constructor.
  apply Hr; auto.
- apply MX.In_Inf; intros.
+ eapply InA_InfA; eauto with *.
+ intros.
  destruct (elements_spec1' r acc y0); intuition.
  intros.
  inversion_clear H.
@@ -1333,7 +1334,7 @@ Hint Resolve elements_spec2.
 
 Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s).
 Proof.
- auto.
+ intros. eapply SortA_NoDupA; eauto with *.
 Qed.
 
 Lemma elements_aux_cardinal :
@@ -1586,7 +1587,7 @@ Proof.
  specialize (IHl2 H).
  specialize (IHr2 H).
  inv.
- MX.elim_compare x1 x2; intros.
+ elim_compare x1 x2.
 
  rewrite H1 by auto; clear H1 IHl2 IHr2.
  unfold Subset. intuition_in.
@@ -1617,7 +1618,7 @@ Proof.
  specialize (IHl2 H).
  specialize (IHr2 H).
  inv.
- MX.elim_compare x1 x2; intros.
+ elim_compare x1 x2.
 
  rewrite H1 by auto; clear H1 IHl2 IHr2.
  unfold Subset. intuition_in.
@@ -1645,7 +1646,7 @@ Proof.
  unfold Subset; intuition_in; try discriminate.
  assert (H': InT x1 Leaf) by auto; inversion H'.
  inv.
- MX.elim_compare x1 x2; intros.
+ elim_compare x1 x2.
 
  rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto.
  clear IHl1 IHr1.
@@ -1751,12 +1752,14 @@ Hint Unfold flip.
 
 (** Correctness of this comparison *)
 
-Definition LCmp := Cmp L.eq L.lt.
+Definition LCmp c x y := Cmp L.eq L.lt x y c.
+
+Hint Unfold LCmp.
 
 Lemma compare_end_Cmp :
  forall e2, LCmp (compare_end e2) nil (flatten_e e2).
 Proof.
- destruct e2; simpl; auto. reflexivity.
+ destruct e2; simpl; constructor; auto. reflexivity.
 Qed.
 
 Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
@@ -1764,8 +1767,7 @@ Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
    LCmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
       (flatten_e (More x2 r2 e2)).
 Proof.
- simpl; intros; MX.elim_compare x1 x2; simpl; auto.
- intros; apply L.cons_Cmp; auto.
+ simpl; intros; elim_compare x1 x2; simpl; auto.
 Qed.
 
 Lemma compare_cont_Cmp : forall s1 cont e2 l,
@@ -1793,11 +1795,10 @@ Proof.
 Qed.
 
 Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2},
- Cmp eq lt (compare s1 s2) s1 s2.
+ Cmp eq lt s1 s2 (compare s1 s2).
 Proof.
  intros.
- generalize (compare_Cmp s1 s2).
- destruct (compare s1 s2); unfold LCmp, Cmp, flip; auto.
+ destruct (compare_Cmp s1 s2); constructor.
  rewrite eq_Leq; auto.
  intros; exists s1, s2; repeat split; auto.
  intros; exists s2, s1; repeat split; auto.
@@ -1810,10 +1811,10 @@ Lemma equal_spec : forall s1 s2 `{Ok s1, Ok s2},
  equal s1 s2 = true <-> eq s1 s2.
 Proof.
 unfold equal; intros s1 s2 B1 B2.
-generalize (@compare_spec s1 s2 B1 B2).
-destruct (compare s1 s2); simpl; split; intros E; auto; try discriminate.
-rewrite E in H. elim (StrictOrder_Irreflexive s2); auto.
-rewrite E in H. elim (StrictOrder_Irreflexive s2); auto.
+destruct (@compare_spec s1 s2 B1 B2) as [H|H|H];
+ split; intros H'; auto; try discriminate.
+rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
+rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto.
 Qed.
 
 End MakeRaw.
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 24eb77e62..49f436a01 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -858,8 +858,7 @@ intros.
 rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros; do 3 (rewrite (fold_add _ _ _);auto).
-rewrite H0;simpl;omega.
+intros; do 3 (rewrite fold_add; auto with *).
 do 3 rewrite fold_empty;auto.
 Qed.
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 831ea0179..a011eb32e 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -29,7 +29,8 @@
     [RawSets] via the use of a subset type (see (W)Raw2Sets below).
 *)
 
-Require Export Bool OrderedType2 DecidableType2.
+Require Export Bool SetoidList RelationClasses Morphisms
+ RelationPairs DecidableType2 OrderedType2 OrderedType2Facts.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -226,7 +227,7 @@ Module Type SetsOn (E : OrderedType).
   Variable s s': t.
   Variable x y : elt.
 
-  Parameter compare_spec : Cmp eq lt (compare s s') s s'.
+  Parameter compare_spec : Cmp eq lt s s' (compare s s').
 
   (** Additional specification of [elements] *)
   Parameter elements_spec2 : sort E.lt (elements s).
@@ -569,7 +570,7 @@ Module Type RawSets (E : OrderedType).
   Variable x y : elt.
 
   (** Specification of [compare] *)
-  Parameter compare_spec : forall `{Ok s, Ok s'}, Cmp eq lt (compare s s') s s'.
+  Parameter compare_spec : forall `{Ok s, Ok s'}, Cmp eq lt s s' (compare s s').
 
   (** Additional specification of [elements] *)
   Parameter elements_spec2 : forall `{Ok s}, sort E.lt (elements s).
@@ -604,11 +605,6 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
 
   (** Specification of [lt] *)
   Instance lt_strorder : StrictOrder lt.
-  Proof.
-  unfold lt; split; repeat red.
-  intros s; eapply StrictOrder_Irreflexive; eauto.
-  intros s s' s''; eapply StrictOrder_Transitive; eauto.
-  Qed.
 
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
   Proof.
@@ -623,10 +619,10 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
   Variable s s' s'' : t.
   Variable x y : elt.
 
-  Lemma compare_spec : Cmp eq lt (compare s s') s s'.
+  Lemma compare_spec : Cmp eq lt s s' (compare s s').
   Proof.
-   generalize (@M.compare_spec s s' _ _).
-   unfold compare; destruct M.compare; auto.
+   assert (H:=@M.compare_spec s s' _ _).
+   unfold compare; destruct M.compare; inversion_clear H; auto.
   Qed.
 
   (** Additional specification of [elements] *)
@@ -752,7 +748,7 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
   left; split; auto.
   rewrite <- (EQ' x); auto.
   (* 2) Pre / Lex *)
-  elim_compare x x'; intros Hxx'.
+  elim_compare x x'.
   (* 2a) x=x' --> Pre *)
   destruct Lex' as (y & INy & LT & Be).
   exists y; split.
@@ -781,16 +777,17 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
   rewrite <- (EQ' y); auto.
   intros z Hz LTz; apply Be; auto. rewrite (EQ' z); auto; order.
   (* 4) Lex / Lex *)
-  elim_compare x x'; intros Hxx'.
+  elim_compare x x'.
   (* 4a) x=x' --> impossible *)
   destruct Lex as (y & INy & LT & Be).
-  rewrite Hxx' in LT; specialize (Be x' IN' LT); order.
+  setoid_replace x with x' in LT; auto.
+  specialize (Be x' IN' LT); order.
   (* 4b) x<x' --> Lex *)
   exists x; split.
   intros z Hz. rewrite <- (EQ' z) by order; auto.
   right; split; auto.
   destruct Lex as (y & INy & LT & Be).
-  elim_compare y x'; intros Hyx'.
+  elim_compare y x'.
    (* 4ba *)
    destruct Lex' as (y' & Iny' & LT' & Be').
    exists y'; repeat split; auto. order.
@@ -802,7 +799,7 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
    rewrite <- (EQ' y); auto.
    intros z Hz LTz. apply Be; auto. rewrite (EQ' z); auto; order.
    (* 4bc*)
-   specialize (Be x' IN' Hyx'); order.
+   assert (O.lt x' x) by auto. order.
   (* 4c) x>x' --> Lex *)
   exists x'; split.
   intros z Hz. rewrite (EQ z) by order; auto.
@@ -879,8 +876,8 @@ End MakeSetOrdering.
 Module MakeListOrdering (O:OrderedType).
  Module MO:=OrderedTypeFacts O.
 
- Notation t := (list O.t).
- Notation In := (InA O.eq).
+ Local Notation t := (list O.t).
+ Local Notation In := (InA O.eq).
 
  Definition eq s s' := forall x, In x s <-> In x s'.
 
@@ -944,9 +941,9 @@ Module MakeListOrdering (O:OrderedType).
  Hint Resolve eq_cons.
 
  Lemma cons_Cmp : forall c x1 x2 l1 l2, O.eq x1 x2 ->
-  Cmp eq lt c l1 l2 -> Cmp eq lt c (x1::l1) (x2::l2).
+  Cmp eq lt l1 l2 c -> Cmp eq lt (x1::l1) (x2::l2) c.
  Proof.
-  destruct c; simpl; unfold flip; auto.
+  destruct c; simpl; inversion_clear 2; auto.
  Qed.
  Hint Resolve cons_Cmp.
 
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 471b43e24..28205e3f6 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -13,7 +13,7 @@
 (** This file proposes an implementation of the non-dependant
     interface [MSetInterface.S] using strictly ordered list. *)
 
-Require Export MSetInterface.
+Require Export MSetInterface OrderedType2Facts OrderedType2Lists.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -206,6 +206,7 @@ End Ops.
 
 Module MakeRaw (X: OrderedType) <: RawSets X.
   Module Import MX := OrderedTypeFacts X.
+  Module Import ML := OrderedTypeLists X.
 
   Include Ops X.
 
@@ -291,7 +292,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction s; intros; inv; simpl.
   intuition. discriminate. inv.
-  elim_compare x a; intros; rewrite InA_cons; intuition; try order.
+  elim_compare x a; rewrite InA_cons; intuition; try order.
   discriminate.
   sort_inf_in. order.
   rewrite <- IHs; auto.
@@ -303,7 +304,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   simple induction s; simpl.
   intuition.
-  intros; elim_compare x a; intros; inv; intuition.
+  intros; elim_compare x a; inv; intuition.
   Qed.
   Hint Resolve add_inf.
 
@@ -311,7 +312,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   simple induction s; simpl.
   intuition.
-  intros; elim_compare x a; intros; inv; auto.
+  intros; elim_compare x a; inv; auto.
   Qed.
 
   Lemma add_spec :
@@ -320,7 +321,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction s; simpl; intros.
   intuition. inv; auto.
-  elim_compare x a; intros; inv; rewrite !InA_cons, ?IHs; intuition.
+  elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
   left; order.
   Qed.
 
@@ -329,7 +330,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction s; simpl.
   intuition.
-  intros; elim_compare x a; intros; inv; auto.
+  intros; elim_compare x a; inv; auto.
   apply Inf_lt with a; auto.
   Qed.
   Hint Resolve remove_inf.
@@ -338,7 +339,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction s; simpl.
   intuition.
-  intros; elim_compare x a; intros; inv; auto.
+  intros; elim_compare x a; inv; auto.
   Qed.
 
   Lemma remove_spec :
@@ -347,7 +348,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction s; simpl; intros.
   intuition; inv; auto.
-  elim_compare x a; intros; inv; rewrite !InA_cons, ?IHs; intuition;
+  elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition;
    try sort_inf_in; try order.
   Qed.
 
@@ -454,7 +455,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv.
   split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv.
   inv.
-  elim_compare x x'; intros C; try discriminate.
+  elim_compare x x' as C; try discriminate.
   (* x=x' *)
   rewrite IH; auto.
   split; intros E y; specialize (E y).
@@ -479,7 +480,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   split; try red; intros; auto.
   split; intros H. discriminate. assert (In x nil) by (apply H; auto). inv.
   split; try red; intros; auto. inv.
-  inv. elim_compare x x'; intros C.
+  inv. elim_compare x x' as C.
   (* x=x' *)
   rewrite IH; auto.
   split; intros S y; specialize (S y).
@@ -750,51 +751,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Instance In_compat : Proper (X.eq==>eq==> iff) In.
   Proof. repeat red; intros; rewrite H, H0; auto. Qed.
 
-(*
-  Module IN <: IN X.
-   Definition t := t.
-   Definition In := In.
-   Instance In_compat : Proper (X.eq==>eq==>iff) In.
-   Proof.
-   intros x x' Ex s s' Es. subst. rewrite Ex; intuition.
-   Qed.
-   Definition Equal := Equal.
-   Definition Empty := Empty.
-  End IN.
-  Include MakeSetOrdering X IN.
-
-  Lemma Ok_Above_Add : forall x s, Ok (x::s) -> Above x s /\ Add x s (x::s).
-  Proof.
-  intros.
-  inver Ok.
-  split.
-  intros y Hy. eapply Sort_Inf_In; eauto.
-  red. intuition. inver In; auto. rewrite <- H2; left; auto.
-  right; auto.
-  Qed.
-
-  Lemma compare_spec :
-   forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'), Cmp eq lt (compare s s') s s'.
-  Proof.
-  induction s as [|x s IH]; intros [|x' s'] Hs Hs'; simpl; intuition.
-  destruct (Ok_Above_Add Hs').
-  eapply lt_empty_l; eauto. intros y Hy. inver InA.
-  destruct (Ok_Above_Add Hs).
-  eapply lt_empty_l; eauto. intros y Hy. inver InA.
-  destruct (Ok_Above_Add Hs); destruct (Ok_Above_Add Hs').
-  inver Ok. unfold Ok in IH. specialize (IH s').
-  elim_compare x x'; intros.
-  destruct (compare s s'); unfold Cmp, flip in IH; auto.
-  intro y; split; intros; inver InA; try (left; order).
-  right; rewrite <- IH; auto.
-  right; rewrite IH; auto.
-  eapply (@lt_add_eq x x'); eauto.
-  eapply (@lt_add_eq x' x); eauto.
-  eapply (@lt_add_lt x x'); eauto.
-  eapply (@lt_add_lt x' x); eauto.
-  Qed.
-*)
-
   Module L := MakeListOrdering X.
   Definition eq := L.eq.
   Definition eq_equiv := L.eq_equiv.
@@ -834,24 +790,20 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
    split; auto. transitivity s4; auto.
   Qed.
 
-  Lemma compare_spec_aux : forall s s', Cmp eq L.lt (compare s s') s s'.
+  Lemma compare_spec_aux : forall s s', Cmp eq L.lt s s' (compare s s').
   Proof.
   induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
-  red; auto.
-  elim_compare x x'; intros; auto.
-  specialize (IH s').
-  destruct (compare s s'); unfold Cmp, flip, eq in IH; auto.
-  apply L.eq_cons; auto.
+  elim_compare x x'; auto.
   Qed.
 
   Lemma compare_spec : forall s s', Ok s -> Ok s' ->
-   Cmp eq lt (compare s s') s s'.
+   Cmp eq lt s s' (compare s s').
   Proof.
   intros s s' Hs Hs'.
   generalize (compare_spec_aux s s').
-  destruct (compare s s'); unfold Cmp, flip in *; auto.
-  exists s, s'; repeat split; auto using @ok.
-  exists s', s; repeat split; auto using @ok.
+  destruct (compare s s'); inversion_clear 1; auto.
+  apply Cmp_lt. exists s, s'; repeat split; auto using @ok.
+  apply Cmp_gt. exists s', s; repeat split; auto using @ok.
   Qed.
 
 End MakeRaw.
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index ab9c69afb..59fbcf49d 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -17,7 +17,7 @@
     [Equal s s'] instead of [equal s s'=true], etc. *)
 
 Require Export MSetInterface.
-Require Import DecidableTypeEx MSetFacts MSetDecide.
+Require Import DecidableTypeEx OrderedType2Lists MSetFacts MSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -762,7 +762,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set.
   Qed.
 
-  Add Morphism cardinal : cardinal_m.
+  Instance cardinal_m : Proper (Equal==>Logic.eq) cardinal.
   Proof.
   exact Equal_cardinal.
   Qed.
@@ -908,7 +908,8 @@ Module Properties := WProperties.
     invalid for Weak Sets. *)
 
 Module OrdProperties (M:Sets).
-  Module ME:=OrderedTypeFacts(M.E).
+  Module Import ME:=OrderedTypeFacts(M.E).
+  Module Import ML:=OrderedTypeLists(M.E).
   Module Import P := Properties M.
   Import FM.
   Import M.E.
@@ -934,13 +935,13 @@ Module OrdProperties (M:Sets).
 
   Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
   Proof.
-   intros; rewrite <- ME.compare_gt_iff. unfold gtb.
+   intros; rewrite <- compare_gt_iff. unfold gtb.
    destruct E.compare; intuition; try discriminate.
   Qed.
 
   Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x.
   Proof.
-   intros; rewrite <- ME.compare_gt_iff. unfold leb, gtb.
+   intros; rewrite <- compare_gt_iff. unfold leb, gtb.
    destruct E.compare; intuition; try discriminate.
   Qed.
 
@@ -963,9 +964,9 @@ Module OrdProperties (M:Sets).
   intros.
   rewrite gtb_1 in H.
   assert (~E.lt y x).
-   unfold gtb in *; ME.elim_compare x y; intuition;
-   try discriminate; ME.order.
-  ME.order.
+   unfold gtb in *; elim_compare x y; intuition;
+   try discriminate; order.
+  order.
   Qed.
 
   Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' ->
@@ -977,29 +978,29 @@ Module OrdProperties (M:Sets).
   apply (@filter_sort _ E.eq); auto with *; eauto with *.
   constructor; auto.
   apply (@filter_sort _ E.eq); auto with *; eauto with *.
-  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with *).
+  rewrite Inf_alt by (apply (@filter_sort _ E.eq); eauto with *).
   intros.
   rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite leb_1 in H2.
   rewrite <- elements_iff in H1.
   assert (~E.eq x y).
    contradict H; rewrite H; auto.
-  ME.order.
+  order.
   intros.
   rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite gtb_1 in H3.
   inversion_clear H2.
-  ME.order.
+  order.
   rewrite filter_InA in H4; auto with *; destruct H4.
   rewrite leb_1 in H4.
-  ME.order.
+  order.
   red; intros a.
   rewrite InA_app_iff, InA_cons, !filter_InA, <-!elements_iff,
    leb_1, gtb_1, (H0 a) by (auto with *).
   intuition.
-  ME.elim_compare a x; intuition.
+  elim_compare a x; intuition.
   right; right; split; auto.
-  ME.order.
+  order.
   Qed.
 
   Definition Above x s := forall y, In y s -> E.lt y x.
@@ -1056,7 +1057,7 @@ Module OrdProperties (M:Sets).
   inversion H0; auto.
   red; intros.
   rewrite remove_iff in H0; destruct H0.
-  generalize (@max_elt_spec2 s e y H H0); ME.order.
+  generalize (@max_elt_spec2 s e y H H0); order.
 
   assert (H0:=max_elt_spec3 H).
   rewrite cardinal_Empty in H0; rewrite H0 in Heqn; inversion Heqn.
@@ -1077,7 +1078,7 @@ Module OrdProperties (M:Sets).
   inversion H0; auto.
   red; intros.
   rewrite remove_iff in H0; destruct H0.
-  generalize (@min_elt_spec2 s e y H H0); ME.order.
+  generalize (@min_elt_spec2 s e y H H0); order.
 
   assert (H0:=min_elt_spec3 H).
   rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn.