Better visibility of the inductive CompSpec used to specify comparison functions

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

21 files changed, 134 insertions, 110 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index a684d5a10..1dc74af73 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -171,7 +171,17 @@ Proof.
    apply -> nat_compare_lt; auto.
 Qed.
 
-(** Some projections of the above equivalences, used in OrderedTypeEx. *)
+Lemma nat_compare_spec : forall x y, CompSpec eq lt x y (nat_compare x y).
+Proof.
+ intros.
+ destruct (nat_compare x y) as [ ]_eqn; constructor.
+ apply nat_compare_eq; auto.
+ apply <- nat_compare_lt; auto.
+ apply <- nat_compare_gt; auto.
+Qed.
+
+
+(** Some projections of the above equivalences. *)
 
 Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m.
 Proof.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 1fb5b3e55..bdd7ce092 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -144,6 +144,13 @@ Proof.
   induction 1; auto with arith.
 Qed.
 
+Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Proof.
+  split.
+  intros; apply le_lt_or_eq; auto.
+  destruct 1; subst; auto with arith.
+Qed.
+
 Theorem lt_le_weak : forall n m, n < m -> n <= m.
 Proof.
   auto with arith.
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index c4e71632c..dda2fca6c 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Peano_dec Compare_dec
+Require Import Lt Peano_dec Compare_dec
  DecidableType2 OrderedType2 OrderedType2Facts.
 
 
@@ -33,26 +33,17 @@ Module Nat_as_OT <: OrderedTypeFull.
  Definition compare := nat_compare.
 
  Instance lt_strorder : StrictOrder lt.
- Proof. split; [ exact Lt.lt_irrefl | exact Lt.lt_trans ]. Qed.
+ Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed.
 
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof. intuition; subst; auto using Lt.le_lt_or_eq. Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
- Proof.
- intros; unfold compare.
- destruct (nat_compare x y) as [ ]_eqn; constructor.
- apply nat_compare_eq; auto.
- apply nat_compare_Lt_lt; auto.
- apply nat_compare_Gt_gt; auto.
- Qed.
+ Definition le_lteq := le_lt_or_eq_iff.
+ Definition compare_spec := nat_compare_spec.
 
 End Nat_as_OT.
 
-(* Note that [Nat_as_OT] can also be seen as a [UsualOrderedType]
+(** Note that [Nat_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)
 
 
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index f6d5ae1ac..4a341328e 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -406,7 +406,7 @@ Module Update_Sets
     | GT _ => Gt
    end.
 
-  Lemma compare_spec : forall s s', Cmp eq lt s s' (compare s s').
+  Lemma compare_spec : forall s s', CompSpec eq lt s s' (compare s s').
   Proof. intros; unfold compare; destruct M.compare; auto. Qed.
 
 End Update_Sets.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 75bf27702..78d0110ae 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -221,6 +221,17 @@ Proof.
   split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto.
 Qed.
 
+(** The [CompSpec] inductive will be used to relate a [compare] function
+    (returning a comparison answer) and some equality and order predicates.
+    Interest: [CompSpec] behave nicely with [destruct]. *)
+
+Inductive CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
+ | CompEq : eq x y -> CompSpec eq lt x y Eq
+ | CompLt : lt x y -> CompSpec eq lt x y Lt
+ | CompGt : lt y x -> CompSpec eq lt x y Gt.
+Hint Constructors CompSpec.
+
+
 (** Identity *)
 
 Definition ID := forall A:Type, A -> A.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 408461a25..477c431c4 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -1752,27 +1752,27 @@ Hint Unfold flip.
 
 (** Correctness of this comparison *)
 
-Definition LCmp c x y := Cmp L.eq L.lt x y c.
+Definition Cmp c x y := CompSpec L.eq L.lt x y c.
 
-Hint Unfold LCmp.
+Hint Unfold Cmp.
 
 Lemma compare_end_Cmp :
- forall e2, LCmp (compare_end e2) nil (flatten_e e2).
+ forall e2, Cmp (compare_end e2) nil (flatten_e e2).
 Proof.
  destruct e2; simpl; constructor; auto. reflexivity.
 Qed.
 
 Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
-  LCmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
-   LCmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
+  Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
+   Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
       (flatten_e (More x2 r2 e2)).
 Proof.
  simpl; intros; elim_compare x1 x2; simpl; auto.
 Qed.
 
 Lemma compare_cont_Cmp : forall s1 cont e2 l,
- (forall e, LCmp (cont e) l (flatten_e e)) ->
- LCmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
+ (forall e, Cmp (cont e) l (flatten_e e)) ->
+ Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
 Proof.
  induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto.
  rewrite <- elements_node; simpl.
@@ -1783,7 +1783,7 @@ Proof.
 Qed.
 
 Lemma compare_Cmp : forall s1 s2,
- LCmp (compare s1 s2) (elements s1) (elements s2).
+ Cmp (compare s1 s2) (elements s1) (elements s2).
 Proof.
  intros; unfold compare.
  rewrite (app_nil_end (elements s1)).
@@ -1795,7 +1795,7 @@ Proof.
 Qed.
 
 Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2},
- Cmp eq lt s1 s2 (compare s1 s2).
+ CompSpec eq lt s1 s2 (compare s1 s2).
 Proof.
  intros.
  destruct (compare_Cmp s1 s2); constructor.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index a011eb32e..ef32c114b 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -227,7 +227,7 @@ Module Type SetsOn (E : OrderedType).
   Variable s s': t.
   Variable x y : elt.
 
-  Parameter compare_spec : Cmp eq lt s s' (compare s s').
+  Parameter compare_spec : CompSpec eq lt s s' (compare s s').
 
   (** Additional specification of [elements] *)
   Parameter elements_spec2 : sort E.lt (elements s).
@@ -570,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 s s' (compare s s').
+  Parameter compare_spec : forall `{Ok s, Ok s'}, CompSpec eq lt s s' (compare s s').
 
   (** Additional specification of [elements] *)
   Parameter elements_spec2 : forall `{Ok s}, sort E.lt (elements s).
@@ -619,7 +619,7 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
   Variable s s' s'' : t.
   Variable x y : elt.
 
-  Lemma compare_spec : Cmp eq lt s s' (compare s s').
+  Lemma compare_spec : CompSpec eq lt s s' (compare s s').
   Proof.
    assert (H:=@M.compare_spec s s' _ _).
    unfold compare; destruct M.compare; inversion_clear H; auto.
@@ -940,11 +940,11 @@ Module MakeListOrdering (O:OrderedType).
  Qed.
  Hint Resolve eq_cons.
 
- Lemma cons_Cmp : forall c x1 x2 l1 l2, O.eq x1 x2 ->
-  Cmp eq lt l1 l2 c -> Cmp eq lt (x1::l1) (x2::l2) c.
+ Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
+  CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.
  Proof.
   destruct c; simpl; inversion_clear 2; auto.
  Qed.
- Hint Resolve cons_Cmp.
+ Hint Resolve cons_CompSpec.
 
 End MakeListOrdering.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 28205e3f6..8b0a16c11 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -790,20 +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 s s' (compare s s').
+  Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
   Proof.
   induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
   elim_compare x x'; auto.
   Qed.
 
   Lemma compare_spec : forall s s', Ok s -> Ok s' ->
-   Cmp eq lt s s' (compare s s').
+   CompSpec eq lt s s' (compare s s').
   Proof.
   intros s s' Hs Hs'.
   generalize (compare_spec_aux s s').
   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.
+  apply CompLt. exists s, s'; repeat split; auto using @ok.
+  apply CompGt. exists s', s; repeat split; auto using @ok.
   Qed.
 
 End MakeRaw.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 813956332..8d589f053 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -427,6 +427,21 @@ pose proof (Pcompare_p_Sq p q) as (_,?);
 assert (p = q <-> Npos p = Npos q); [split; congruence | tauto].
 Qed.
 
+Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y.
+Proof.
+unfold Nle, Nlt; intros.
+generalize (Ncompare_eq_correct x y).
+destruct (x ?= y); intuition; discriminate.
+Qed.
+
+Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y).
+Proof.
+intros.
+destruct (Ncompare x y) as [ ]_eqn; constructor; auto.
+apply Ncompare_Eq_eq; auto.
+apply Ngt_Nlt; auto.
+Qed.
+
 (** 0 is the least natural number *)
 
 Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 20cfb43a3..7e3523a8c 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -857,6 +857,15 @@ Proof.
   symmetry; apply Pcompare_antisym.
 Qed.
 
+Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq).
+Proof.
+  intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor.
+  apply Pcompare_Eq_eq; auto.
+  auto.
+  apply ZC1; auto.
+Qed.
+
+
 (** Comparison and the successor *)
 
 Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
@@ -932,6 +941,14 @@ Proof.
   destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto.
 Qed.
 
+Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q.
+Proof.
+  unfold Ple, Plt. intros.
+  generalize (Pcompare_eq_iff p q).
+  destruct ((p ?= q) Eq); intuition; discriminate.
+Qed.
+
+
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
index 8f69cd656..bd701cbea 100644
--- a/theories/NArith/NOrderedType.v
+++ b/theories/NArith/NOrderedType.v
@@ -39,23 +39,12 @@ Module N_as_OT <: OrderedTypeFull.
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Nlt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof.
- unfold Nle, Nlt; intros. rewrite <- Ncompare_eq_correct.
- destruct (x ?= y); intuition; discriminate.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (Ncompare x y).
- Proof.
- intros.
- destruct (Ncompare x y) as [ ]_eqn; constructor; auto.
- apply Ncompare_Eq_eq; auto.
- apply Ngt_Nlt; auto.
- Qed.
+ Definition le_lteq := Nle_lteq.
+ Definition compare_spec := Ncompare_spec.
 
 End N_as_OT.
 
-(* Note that [N_as_OT] can also be seen as a [UsualOrderedType]
+(** Note that [N_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)
 
 
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
index 2f89b0e68..a4eeb9b97 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/NArith/POrderedType.v
@@ -39,25 +39,12 @@ Module Positive_as_OT <: OrderedTypeFull.
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Plt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof.
- unfold Ple, Plt. intros.
- rewrite <- Pcompare_eq_iff.
- destruct (Pcompare x y Eq); intuition; discriminate.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
- Proof.
- intros; unfold compare.
- destruct (Pcompare x y Eq) as [ ]_eqn; constructor.
- apply Pcompare_Eq_eq; auto.
- auto.
- apply ZC1; auto.
- Qed.
+ Definition le_lteq := Ple_lteq.
+ Definition compare_spec := Pcompare_spec.
 
 End Positive_as_OT.
 
-(* Note that [Positive_as_OT] can also be seen as a [UsualOrderedType]
+(** Note that [Positive_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)
 
 
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 70830ad80..609241d5e 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -87,6 +87,19 @@ Qed.
 Hint Unfold Qeq Qlt Qle : qarith.
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
+Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x).
+Proof.
+ unfold "?=". intros. apply Zcompare_antisym.
+Qed.
+
+Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y).
+Proof.
+ intros.
+ destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
+ rewrite Qeq_alt; auto.
+ rewrite Qlt_alt, <- Qcompare_antisym, H; auto.
+Qed.
+
 (** * Properties of equality. *)
 
 Theorem Qeq_refl : forall x, x == x.
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index 3d83eac38..f6f457f65 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.v
@@ -42,19 +42,7 @@ Module Q_as_OT <: OrderedTypeFull.
  Proof. auto with *. Qed.
 
  Definition le_lteq := Qle_lteq.
-
- Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x).
- Proof.
- unfold "?=". intros. apply Zcompare_antisym.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp Qeq Qlt x y (Qcompare x y).
- Proof.
- intros.
- destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
- rewrite Qeq_alt; auto.
- rewrite Qlt_alt, <- Qcompare_antisym, H; auto.
- Qed.
+ Definition compare_spec := Qcompare_spec.
 
 End Q_as_OT.
 
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 4d62c2716..310f99a4a 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -14,14 +14,6 @@ Unset Strict Implicit.
 
 (** * Ordered types *)
 
-Inductive Cmp {A} (eq lt:relation A)(x y : A) : comparison -> Prop :=
-| Cmp_eq : eq x y -> Cmp eq lt x y Eq
-| Cmp_lt : lt x y -> Cmp eq lt x y Lt
-| Cmp_gt : lt y x -> Cmp eq lt x y Gt.
-
-Hint Constructors Cmp.
-
-
 Module Type MiniOrderedType.
   Include Type EqualityType.
 
@@ -29,8 +21,8 @@ Module Type MiniOrderedType.
   Instance lt_strorder : StrictOrder lt.
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
-  Parameter compare : t -> t -> comparison.
-  Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y).
+  Parameter Inline compare : t -> t -> comparison.
+  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 
 End MiniOrderedType.
 
@@ -76,8 +68,8 @@ Module Type UsualOrderedType.
     for subtyping... *)
  Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
- Parameter compare : t -> t -> comparison.
- Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ Parameter Inline compare : t -> t -> comparison.
+ Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 
 End UsualOrderedType.
 
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v
index 4e14f5128..43b27553f 100644
--- a/theories/Structures/OrderedType2Alt.v
+++ b/theories/Structures/OrderedType2Alt.v
@@ -76,7 +76,7 @@ Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
     | GT _ => Gt
   end.
 
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
   intros; unfold compare; destruct O.compare; auto.
  Qed.
@@ -169,11 +169,11 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
 
  Definition compare := O.compare.
 
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ 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 Cmp_gt.
+  apply CompGt.
   rewrite compare_sym, H; auto.
  Qed.
 
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v
index 801c18723..6a0231973 100644
--- a/theories/Structures/OrderedType2Ex.v
+++ b/theories/Structures/OrderedType2Ex.v
@@ -77,7 +77,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
    | Gt => Gt
   end.
 
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ 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).
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v
index 382b6366d..a7bb661ea 100644
--- a/theories/Structures/OrderedType2Facts.v
+++ b/theories/Structures/OrderedType2Facts.v
@@ -254,7 +254,7 @@ Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
 
 Definition compare := flip O.compare.
 
-Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+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.
diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v
index 6e30e0bf8..34456dcf9 100644
--- a/theories/ZArith/ZOrderedType.v
+++ b/theories/ZArith/ZOrderedType.v
@@ -39,24 +39,12 @@ Module Z_as_OT <: OrderedTypeFull.
  Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Zlt.
  Proof. repeat red; intros; subst; auto. Qed.
 
- Lemma le_lteq : forall x y, x <= y <-> x < y \/ x=y.
- Proof.
- unfold le, lt, Zle, Zlt. intros.
- rewrite <- Zcompare_Eq_iff_eq.
- destruct (x ?= y); intuition; discriminate.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp eq lt x y (Zcompare x y).
- Proof.
- intros; unfold compare.
- destruct (Zcompare x y) as [ ]_eqn; constructor; auto.
- apply Zcompare_Eq_eq; auto.
- apply Zgt_lt; auto.
- Qed.
+ Definition le_lteq := Zle_lt_or_eq_iff.
+ Definition compare_spec := Zcompare_spec.
 
 End Z_as_OT.
 
-(* Note that [Z_as_OT] can also be seen as a [UsualOrderedType]
+(** Note that [Z_as_OT] can also be seen as a [UsualOrderedType]
    and a [OrderedType] (and also as a [DecidableType]). *)
 
 
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 2515b7f7b..3e611d543 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -72,6 +72,15 @@ Proof.
   intros; f_equal; auto.
 Qed.
 
+Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m).
+Proof.
+  intros.
+  destruct (n?=m) as [ ]_eqn:H; constructor; auto.
+  apply Zcompare_Eq_eq; auto.
+  red; rewrite <- Zcompare_antisym, H; auto.
+Qed.
+
+
 (** * Transitivity of comparison *)
 
 Lemma Zcompare_Lt_trans :
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 70cbe0f28..0db71e68d 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -257,6 +257,13 @@ Proof.
       | absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption ].
 Qed.
 
+Lemma Zle_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Proof.
+  unfold Zle, Zlt. intros.
+  generalize (Zcompare_Eq_iff_eq n m).
+  destruct (n ?= m); intuition; discriminate.
+Qed.
+
 (** Dichotomy *)
 
 Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n.