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

1 files changed, 14 insertions, 10 deletions

diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 4c2a19f69..ee9051ff8 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -166,19 +166,23 @@ Definition leb x y :=
     | _ => true
   end.
 
-Definition geb x y := (* TODO : to provide ? to modify ? *)
-  match x ?= y with
-    | Lt => false
-    | _ => true
-  end.
-
 Definition ltb x y :=
   match x ?= y with
     | Lt => true
     | _ => false
   end.
 
-Definition gtb x y := (* TODO : to provide ? to modify ? *)
+(** Nota: [geb] and [gtb] are provided for compatibility,
+  but [leb] and [ltb] should rather be used instead, since
+  more results we be available on them. *)
+
+Definition geb x y :=
+  match x ?= y with
+    | Lt => false
+    | _ => true
+  end.
+
+Definition gtb x y :=
   match x ?= y with
     | Gt => true
     | _ => false
@@ -322,15 +326,15 @@ Definition iter (n:Z) {A} (f:A -> A) (x:A) :=
 
 Fixpoint pos_div_eucl (a:positive) (b:Z) : Z * Z :=
   match a with
-    | xH => if b >=? 2 then (0, 1) else (1, 0)
+    | xH => if 2 <=? b then (0, 1) else (1, 0)
     | xO a' =>
       let (q, r) := pos_div_eucl a' b in
       let r' := 2 * r in
-      if b >? r' then (2 * q, r') else (2 * q + 1, r' - b)
+      if r' <? b then (2 * q, r') else (2 * q + 1, r' - b)
     | xI a' =>
       let (q, r) := pos_div_eucl a' b in
       let r' := 2 * r + 1 in
-      if b >? r' then (2 * q, r') else (2 * q + 1, r' - b)
+      if r' <? b then (2 * q, r') else (2 * q + 1, r' - b)
   end.
 
 (** Then the general euclidean division *)