Arithemtic: more concerning compare, eqb, leb, ltb

 Start of a uniform treatment of compare, eqb, leb, ltb:
 - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
 - Some generic properties are derived in OrdersFacts.BoolOrderFacts

 In BinPos, more work about sub_mask with nice implications
 on compare (e.g. simplier proof of lt_trans).

 In BinNat/BinPos, for uniformity, compare_antisym is now
 (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.

 In BigN / BigZ, eq_bool is now eqb

 In BinIntDef, gtb and geb are kept for the moment, but
 a comment advise to rather use ltb and leb. Z.div now uses
 Z.ltb and Z.leb.

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

3 files changed, 386 insertions, 97 deletions

diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 2fbdff624..933c4ea0e 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -66,10 +66,19 @@ End HasEqDec.
 (** Having [eq_dec] is the same as having a boolean equality plus
     a correctness proof. *)
 
-Module Type HasEqBool (Import E:Eq').
+Module Type HasEqb (Import T:Typ).
   Parameter Inline eqb : t -> t -> bool.
-  Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
-End HasEqBool.
+End HasEqb.
+
+Module Type EqbSpec (T:Typ)(X:HasEq T)(Y:HasEqb T).
+  Parameter eqb_eq : forall x y, Y.eqb x y = true <-> X.eq x y.
+End EqbSpec.
+
+Module Type EqbNotation (T:Typ)(E:HasEqb T).
+  Infix "=?" := E.eqb (at level 70, no associativity).
+End EqbNotation.
+
+Module Type HasEqBool (E:Eq) := HasEqb E <+ EqbSpec E E.
 
 (** From these basic blocks, we can build many combinations
     of static standalone module types. *)
@@ -107,8 +116,10 @@ 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 BooleanEqualityType' :=
+ BooleanEqualityType <+ EqNotation <+ EqbNotation.
+Module Type BooleanDecidableType' :=
+ BooleanDecidableType <+ EqNotation <+ EqbNotation.
 Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
 
 (** * Compatibility wrapper from/to the old version of
@@ -166,9 +177,12 @@ Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
 Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
  := E <+ HasEqBool2Dec.
 
-(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
 
-Module BoolEqualityFacts (Import E : BooleanEqualityType).
+(** Some properties of boolean equality *)
+
+Module BoolEqualityFacts (Import E : BooleanEqualityType').
+
+(** [eqb] is compatible with [eq] *)
 
 Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
 Proof.
@@ -177,6 +191,34 @@ apply eq_true_iff_eq.
 now rewrite 2 eqb_eq, Exx', Eyy'.
 Qed.
 
+(** Alternative specification of [eqb] based on [reflect]. *)
+
+Lemma eqb_spec x y : reflect (x==y) (x =? y).
+Proof.
+apply iff_reflect. symmetry. apply eqb_eq.
+Qed.
+
+(** Negated form of [eqb_eq] *)
+
+Lemma eqb_neq x y : (x =? y) = false <-> x ~= y.
+Proof.
+now rewrite <- not_true_iff_false, eqb_eq.
+Qed.
+
+(** Basic equality laws for [eqb] *)
+
+Lemma eqb_refl x : (x =? x) = true.
+Proof.
+now apply eqb_eq.
+Qed.
+
+Lemma eqb_sym x y : (x =? y) = (y =? x).
+Proof.
+apply eq_true_iff_eq. now rewrite 2 eqb_eq.
+Qed.
+
+(** Transitivity is a particular case of [eqb_compat] *)
+
 End BoolEqualityFacts.
 
 
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 99dfb19d5..1d0254397 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -65,20 +65,34 @@ 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').
+Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
+Module Type StrOrder' := StrOrder <+ EqLtNotation.
+
+(** Versions with a decidable ternary comparison *)
+
+Module Type HasCmp (Import T:Typ).
   Parameter Inline compare : t -> t -> comparison.
+End HasCmp.
+
+Module Type CmpNotation (T:Typ)(C:HasCmp T).
+  Infix "?=" := C.compare (at level 70, no associativity).
+End CmpNotation.
+
+Module Type CmpSpec (Import E:EqLt')(Import C:HasCmp E).
   Axiom compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
-End HasCompare.
+End CmpSpec.
+
+Module Type HasCompare (E:EqLt) := HasCmp E <+ CmpSpec E.
 
-Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
 Module Type DecStrOrder := StrOrder <+ HasCompare.
+Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation <+ CmpNotation.
+
 Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
-Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
+Module Type OrderedType' := OrderedType <+ EqLtNotation <+ CmpNotation.
 
-Module Type StrOrder' := StrOrder <+ EqLtNotation.
-Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
-Module Type OrderedType' := OrderedType <+ EqLtNotation.
-Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.
+Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
+Module Type OrderedTypeFull' :=
+ OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation.
 
 (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
   But adding this redundant field allows to see an [OrderedType] as a
@@ -167,50 +181,63 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
 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 HasLeb (Import T:Typ).
+ Parameter Inline leb : t -> t -> bool.
+End HasLeb.
 
-Module Type LeBool := Typ <+ HasLeBool.
-Module Type LtBool := Typ <+ HasLtBool.
+Module Type HasLtb (Import T:Typ).
+ Parameter Inline ltb : t -> t -> bool.
+End HasLtb.
 
-Module Type LeBoolNotation (E:LeBool).
-  Infix "<=?" := E.leb (at level 35).
-End LeBoolNotation.
+Module Type LebNotation (T:Typ)(E:HasLeb T).
+ Infix "<=?" := E.leb (at level 35).
+End LebNotation.
 
-Module Type LtBoolNotation (E:LtBool).
-  Infix "<?" := E.ltb (at level 35).
-End LtBoolNotation.
+Module Type LtbNotation (T:Typ)(E:HasLtb T).
+ Infix "<?" := E.ltb (at level 35).
+End LtbNotation.
 
-Module Type LeBool' := LeBool <+ LeBoolNotation.
-Module Type LtBool' := LtBool <+ LtBoolNotation.
+Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T).
+ Parameter leb_le : forall x y, Y.leb x y = true <-> X.le x y.
+End LebSpec.
 
-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 LtbSpec (T:Typ)(X:HasLt T)(Y:HasLtb T).
+ Parameter ltb_lt : forall x y, Y.ltb x y = true <-> X.lt x y.
+End LtbSpec.
 
-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 LeBool := Typ <+ HasLeb.
+Module Type LtBool := Typ <+ HasLtb.
+Module Type LeBool' := LeBool <+ LebNotation.
+Module Type LtBool' := LtBool <+ LtbNotation.
 
-Module Type LeBoolIsTotal (Import X:LeBool').
+Module Type LebIsTotal (Import X:LeBool').
  Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true.
-End LeBoolIsTotal.
+End LebIsTotal.
 
-Module Type TotalLeBool := LeBool <+ LeBoolIsTotal.
-Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal.
+Module Type TotalLeBool := LeBool <+ LebIsTotal.
+Module Type TotalLeBool' := LeBool' <+ LebIsTotal.
 
-Module Type LeBoolIsTransitive (Import X:LeBool').
+Module Type LebIsTransitive (Import X:LeBool').
  Axiom leb_trans : Transitive X.leb.
-End LeBoolIsTransitive.
+End LebIsTransitive.
+
+Module Type TotalTransitiveLeBool := TotalLeBool <+ LebIsTransitive.
+Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LebIsTransitive.
+
+(** Grouping all boolean comparison functions *)
+
+Module Type HasBoolOrdFuns (T:Typ) := HasEqb T <+ HasLtb T <+ HasLeb T.
+
+Module Type HasBoolOrdFuns' (T:Typ) :=
+ HasBoolOrdFuns T <+ EqbNotation T <+ LtbNotation T <+ LebNotation T.
 
-Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive.
-Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive.
+Module Type BoolOrdSpecs (O:EqLtLe)(F:HasBoolOrdFuns O) :=
+ EqbSpec O O F <+ LtbSpec O O F <+ LebSpec O O F.
 
+Module Type OrderFunctions (E:EqLtLe) :=
+  HasCompare E <+ HasBoolOrdFuns E <+ BoolOrdSpecs E.
+Module Type OrderFunctions' (E:EqLtLe) :=
+  HasCompare E <+ CmpNotation E <+ HasBoolOrdFuns' E <+ BoolOrdSpecs E.
 
 (** * From [OrderedTypeFull] to [TotalTransitiveLeBool] *)
 
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index b328ae2e8..a447e8fb5 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -6,15 +6,76 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import Basics OrdersTac.
+Require Import Bool Basics OrdersTac.
 Require Export Orders.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Properties of [OrderedTypeFull] *)
+(** * Properties of [compare] *)
 
-Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
+Module Type CompareFacts (Import O:DecStrOrder').
+
+ Local Infix "?=" := compare (at level 70, no associativity).
+
+ Lemma compare_eq_iff x y : (x ?= y) = Eq <-> x==y.
+ Proof.
+ case compare_spec; intro H; split; try easy; intro EQ;
+  contradict H; rewrite EQ; apply irreflexivity.
+ Qed.
+
+ Lemma compare_eq x y : (x ?= y) = Eq -> x==y.
+ Proof.
+ apply compare_eq_iff.
+ Qed.
+
+ Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y.
+ Proof.
+ case compare_spec; intro H; split; try easy; intro LT;
+  contradict LT; rewrite H; apply irreflexivity.
+ Qed.
+
+ Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x.
+ Proof.
+ case compare_spec; intro H; split; try easy; intro LT;
+  contradict LT; rewrite H; apply irreflexivity.
+ Qed.
+
+ Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y).
+ Proof.
+ rewrite compare_lt_iff; intuition.
+ Qed.
+
+ Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x).
+ Proof.
+ 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'.
+ case (compare_spec x' y'); autorewrite with order; now rewrite Hxx', Hyy'.
+ Qed.
+
+ Lemma compare_refl x : (x ?= x) = Eq.
+ Proof.
+ case compare_spec; intros; trivial; now elim irreflexivity with x.
+ Qed.
+
+ Lemma compare_antisym x y : (y ?= x) = CompOpp (x ?= y).
+ Proof.
+ case (compare_spec x y); simpl; autorewrite with order;
+  trivial; now symmetry.
+ Qed.
+
+End CompareFacts.
+
+
+ (** * Properties of [OrderedTypeFull] *)
+
+Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull').
 
  Module OrderTac := OTF_to_OrderTac O.
  Ltac order := OrderTac.order.
@@ -47,6 +108,18 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
  Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
  Proof. iorder. Qed.
 
+ Include CompareFacts O.
+
+ Lemma compare_le_iff x y : compare x y <> Gt <-> x<=y.
+ Proof.
+ rewrite le_not_gt_iff. apply compare_ngt_iff.
+ Qed.
+
+ Lemma compare_ge_iff x y : compare x y <> Lt <-> y<=x.
+ Proof.
+ rewrite le_not_gt_iff. apply compare_nlt_iff.
+ Qed.
+
 End OrderedTypeFullFacts.
 
 
@@ -84,50 +157,9 @@ Module OrderedTypeFacts (Import O: OrderedType').
 
   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.
+  Include CompareFacts O.
+  Notation compare_le_iff := compare_ngt_iff (only parsing).
+  Notation compare_ge_iff := compare_nlt_iff (only parsing).
 
   (** For compatibility reasons *)
   Definition eq_dec := eq_dec.
@@ -162,10 +194,6 @@ Module OrderedTypeFacts (Import O: OrderedType').
 End OrderedTypeFacts.
 
 
-
-
-
-
 (** * Tests of the order tactic
 
     Is it at least capable of proving some basic properties ? *)
@@ -232,3 +260,195 @@ Qed.
 
 End OrderedTypeRev.
 
+Unset Implicit Arguments.
+
+(** * Order relations derived from a [compare] function.
+
+  We factorize here some common properties for ZArith, NArith
+  and co, where [lt] and [le] are defined in terms of [compare].
+  Note that we do not require anything here concerning compatibility
+  of [compare] w.r.t [eq], nor anything concerning transitivity.
+*)
+
+Module Type CompareBasedOrder (Import E:EqLtLe')(Import C:HasCmp E).
+ Include CmpNotation E C.
+ Include IsEq E.
+ Axiom compare_eq_iff : forall x y, (x ?= y) = Eq <-> x == y.
+ Axiom compare_lt_iff : forall x y, (x ?= y) = Lt <-> x < y.
+ Axiom compare_le_iff : forall x y, (x ?= y) <> Gt <-> x <= y.
+ Axiom compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
+End CompareBasedOrder.
+
+Module Type CompareBasedOrderFacts
+ (Import E:EqLtLe')
+ (Import C:HasCmp E)
+ (Import O:CompareBasedOrder E C).
+
+ Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y).
+ Proof.
+  case_eq (compare x y); intros H; constructor.
+  now apply compare_eq_iff.
+  now apply compare_lt_iff.
+  rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff.
+ Qed.
+
+ Lemma compare_eq x y : (x ?= y) = Eq -> x==y.
+ Proof.
+ apply compare_eq_iff.
+ Qed.
+
+ Lemma compare_refl x : (x ?= x) = Eq.
+ Proof.
+ now apply compare_eq_iff.
+ Qed.
+
+ Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x.
+ Proof.
+ now rewrite <- compare_lt_iff, compare_antisym, CompOpp_iff.
+ Qed.
+
+ Lemma compare_ge_iff x y : (x ?= y) <> Lt <-> y<=x.
+ Proof.
+ now rewrite <- compare_le_iff, compare_antisym, CompOpp_iff.
+ Qed.
+
+ Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x).
+ Proof.
+ rewrite compare_gt_iff; intuition.
+ Qed.
+
+ Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y).
+ Proof.
+ rewrite compare_lt_iff; intuition.
+ Qed.
+
+ Lemma compare_nle_iff x y : (x ?= y) = Gt <-> ~(x<=y).
+ Proof.
+ rewrite <- compare_le_iff.
+ destruct compare; split; easy || now destruct 1.
+ Qed.
+
+ Lemma compare_nge_iff x y : (x ?= y) = Lt <-> ~(y<=x).
+ Proof.
+ now rewrite <- compare_nle_iff, compare_antisym, CompOpp_iff.
+ Qed.
+
+ Lemma lt_irrefl x : ~ (x<x).
+ Proof.
+ now rewrite <- compare_lt_iff, compare_refl.
+ Qed.
+
+ Lemma lt_eq_cases n m : n <= m <-> n < m \/ n==m.
+ Proof.
+ rewrite <- compare_lt_iff, <- compare_le_iff, <- compare_eq_iff.
+ destruct (n ?= m); now intuition.
+ Qed.
+
+End CompareBasedOrderFacts.
+
+(** Basic facts about boolean comparisons *)
+
+Module Type BoolOrderFacts
+ (Import E:EqLtLe')
+ (Import C:HasCmp E)
+ (Import F:HasBoolOrdFuns' E)
+ (Import O:CompareBasedOrder E C)
+ (Import S:BoolOrdSpecs E F).
+
+Include CompareBasedOrderFacts E C O.
+
+(** Nota : apart from [eqb_compare] below, facts about [eqb]
+  are in BoolEqualityFacts *)
+
+(** Alternate specifications based on [BoolSpec] and [reflect] *)
+
+Lemma leb_spec0 x y : reflect (x<=y) (x<=?y).
+Proof.
+ apply iff_reflect. symmetry. apply leb_le.
+Qed.
+
+Lemma leb_spec x y : BoolSpec (x<=y) (y<x) (x<=?y).
+Proof.
+ case leb_spec0; constructor; trivial.
+ now rewrite <- compare_lt_iff, compare_nge_iff.
+Qed.
+
+Lemma ltb_spec0 x y : reflect (x<y) (x<?y).
+Proof.
+ apply iff_reflect. symmetry. apply ltb_lt.
+Qed.
+
+Lemma ltb_spec x y : BoolSpec (x<y) (y<=x) (x<?y).
+Proof.
+ case ltb_spec0; constructor; trivial.
+ now rewrite <- compare_le_iff, compare_ngt_iff.
+Qed.
+
+(** Negated variants of the specifications *)
+
+Lemma leb_nle x y : x <=? y = false <-> ~ (x <= y).
+Proof.
+now rewrite <- not_true_iff_false, leb_le.
+Qed.
+
+Lemma leb_gt x y : x <=? y = false <-> y < x.
+Proof.
+now rewrite leb_nle, <- compare_lt_iff, compare_nge_iff.
+Qed.
+
+Lemma ltb_nlt x y : x <? y = false <-> ~ (x < y).
+Proof.
+now rewrite <- not_true_iff_false, ltb_lt.
+Qed.
+
+Lemma ltb_ge x y : x <? y = false <-> y <= x.
+Proof.
+now rewrite ltb_nlt, <- compare_le_iff, compare_ngt_iff.
+Qed.
+
+(** Basic equality laws for boolean tests *)
+
+Lemma leb_refl x : x <=? x = true.
+Proof.
+apply leb_le. apply lt_eq_cases. now right.
+Qed.
+
+Lemma leb_antisym x y : y <=? x = negb (x <? y).
+Proof.
+apply eq_true_iff_eq. now rewrite negb_true_iff, leb_le, ltb_ge.
+Qed.
+
+Lemma ltb_irrefl x : x <? x = false.
+Proof.
+apply ltb_ge. apply lt_eq_cases. now right.
+Qed.
+
+Lemma ltb_antisym x y : y <? x = negb (x <=? y).
+Proof.
+apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt.
+Qed.
+
+(** Relation bewteen [compare] and the boolean comparisons *)
+
+Lemma eqb_compare x y :
+ (x =? y) = match compare x y with Eq => true | _ => false end.
+Proof.
+apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff.
+destruct compare; now split.
+Qed.
+
+Lemma ltb_compare x y :
+ (x <? y) = match compare x y with Lt => true | _ => false end.
+Proof.
+apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff.
+destruct compare; now split.
+Qed.
+
+Lemma leb_compare x y :
+ (x <=? y) = match compare x y with Gt => false | _ => true end.
+Proof.
+apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff.
+destruct compare; split; try easy. now destruct 1.
+Qed.
+
+End BoolOrderFacts.