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

12 files changed, 332 insertions, 177 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 237ac93ef..a5be98aab 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -111,14 +111,12 @@ Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.
 
 (** Let's group everything *)
 
-Module Type ZAxiomsSig :=
-  ZAxiomsMiniSig <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn
-   <+ NZParity.NZParity
+Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions
+   <+ HasAbs <+ HasSgn <+ NZParity.NZParity
    <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
    <+ ZDiv <+ ZQuot <+ NZBits.NZBits.
 
-Module Type ZAxiomsSig' :=
-  ZAxiomsMiniSig' <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn
-   <+ NZParity.NZParity
+Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions'
+   <+ HasAbs <+ HasSgn <+ NZParity.NZParity
    <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
    <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 236c56b9f..71d275601 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -56,6 +56,9 @@ Infix "*" := BigZ.mul : bigZ_scope.
 Infix "/" := BigZ.div : bigZ_scope.
 Infix "^" := BigZ.pow : bigZ_scope.
 Infix "?=" := BigZ.compare : bigZ_scope.
+Infix "=?" := BigZ.eqb (at level 70, no associativity) : bigZ_scope.
+Infix "<=?" := BigZ.leb (at level 70, no associativity) : bigZ_scope.
+Infix "<?" := BigZ.ltb (at level 70, no associativity) : bigZ_scope.
 Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
 Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope.
 Infix "<" := BigZ.lt : bigZ_scope.
@@ -112,7 +115,7 @@ symmetry. apply BigZ.add_opp_r.
 exact BigZ.add_opp_diag_r.
 Qed.
 
-Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y.
+Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y.
 Proof. now apply BigZ.eqb_eq. Qed.
 
 Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n).
@@ -127,11 +130,11 @@ induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto.
 Qed.
 
 Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _)
- (fun a b => if BigZ.eq_bool b 0 then (0,a) else BigZ.div_eucl a b).
+ (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b).
 Proof.
 constructor. unfold id. intros a b.
 BigZ.zify.
-generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+case Z.eqb_spec.
 BigZ.zify. auto with zarith.
 intros NEQ.
 generalize (BigZ.spec_div_eucl a b).
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index da501e9ef..8e53e4d62 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -109,21 +109,49 @@ Module Make (N:NType) <: ZType.
   exfalso. omega.
  Qed.
 
- Definition eq_bool x y :=
+ Definition eqb x y :=
   match compare x y with
   | Eq => true
   | _ => false
   end.
 
- Theorem spec_eq_bool:
-  forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y).
+ Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y).
  Proof.
- unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity.
+ apply Bool.eq_iff_eq_true.
+ unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare.
+ split; [now destruct Z.compare | now intros ->].
  Qed.
 
  Definition lt n m := to_Z n < to_Z m.
  Definition le n m := to_Z n <= to_Z m.
 
+
+ Definition ltb (x y : t) : bool :=
+  match compare x y with
+  | Lt => true
+  | _  => false
+  end.
+
+ Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare.
+ split; [now destruct Z.compare | now intros ->].
+ Qed.
+
+ Definition leb (x y : t) : bool :=
+  match compare x y with
+  | Gt => false
+  | _  => true
+  end.
+
+ Theorem spec_leb x y : leb x y = Z.leb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
+ destruct Z.compare; split; try easy. now destruct 1.
+ Qed.
+
  Definition min n m := match compare n m with Gt => m | _ => n end.
  Definition max n m := match compare n m with Lt => m | _ => n end.
 
@@ -372,12 +400,12 @@ Module Make (N:NType) <: ZType.
     (Pos q, Pos r)
   | Pos nx, Neg ny =>
     let (q, r) := N.div_eucl nx ny in
-    if N.eq_bool N.zero r
+    if N.eqb N.zero r
     then (Neg q, zero)
     else (Neg (N.succ q), Neg (N.sub ny r))
   | Neg nx, Pos ny =>
     let (q, r) := N.div_eucl nx ny in
-    if N.eq_bool N.zero r
+    if N.eqb N.zero r
     then (Neg q, zero)
     else (Neg (N.succ q), Pos (N.sub ny r))
   | Neg nx, Neg ny =>
@@ -401,32 +429,32 @@ Module Make (N:NType) <: ZType.
  (* Pos Neg *)
  generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
       simpl; rewrite Hq, N.spec_0; auto).
  change (- Zpos py) with (Zneg py).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
  intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
  rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
  (* Neg Pos *)
  generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
       simpl; rewrite Hq, N.spec_0; auto).
  change (- Zpos px) with (Zneg px).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
  intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
  rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
  (* Neg Neg *)
  generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
@@ -464,7 +492,7 @@ Module Make (N:NType) <: ZType.
   end.
 
  Definition rem x y :=
-  if eq_bool y zero then x
+  if eqb y zero then x
   else
     match x, y with
       | Pos nx, Pos ny => Pos (N.modulo nx ny)
@@ -483,8 +511,8 @@ Module Make (N:NType) <: ZType.
  Lemma spec_rem : forall x y,
    to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
  Proof.
-  intros x y. unfold rem. rewrite spec_eq_bool, spec_0.
-  assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
+  intros x y. unfold rem. rewrite spec_eqb, spec_0.
+  case Z.eqb_spec; intros Hy.
   now rewrite Hy, Zrem_0_r.
   destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
    rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive;
@@ -551,7 +579,7 @@ Module Make (N:NType) <: ZType.
  Definition norm_pos z :=
    match z with
      | Pos _ => z
-     | Neg n => if N.eq_bool n N.zero then Pos n else z
+     | Neg n => if N.eqb n N.zero then Pos n else z
    end.
 
  Definition testbit a n :=
@@ -623,19 +651,17 @@ Module Make (N:NType) <: ZType.
  Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x.
  Proof.
   intros [x|x]; simpl; trivial.
-  rewrite N.spec_eq_bool, N.spec_0.
-  assert (H := Zeq_bool_if (N.to_Z x) 0).
-  destruct Zeq_bool; simpl; auto with zarith.
+  rewrite N.spec_eqb, N.spec_0.
+  case Z.eqb_spec; simpl; auto with zarith.
  Qed.
 
  Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y ->
   0 < N.to_Z y.
  Proof.
   intros [x|x] y; simpl; try easy.
-  rewrite N.spec_eq_bool, N.spec_0.
-  assert (H := Zeq_bool_if (N.to_Z x) 0).
-  destruct Zeq_bool; simpl; try easy.
-  inversion 1; subst. generalize (N.spec_pos y); auto with zarith.
+  rewrite N.spec_eqb, N.spec_0.
+  case Z.eqb_spec; simpl; try easy.
+  inversion 2. subst. generalize (N.spec_pos y); auto with zarith.
  Qed.
 
  Ltac destr_norm_pos x :=
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 9981fab71..0f2862df7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Znumtheory.
+Require Import BinInt.
 
 Open Scope Z_scope.
 
@@ -33,7 +33,9 @@ Module Type ZType.
  Parameter spec_of_Z: forall x, to_Z (of_Z x) = x.
 
  Parameter compare : t -> t -> comparison.
- Parameter eq_bool : t -> t -> bool.
+ Parameter eqb : t -> t -> bool.
+ Parameter ltb : t -> t -> bool.
+ Parameter leb : t -> t -> bool.
  Parameter min : t -> t -> t.
  Parameter max : t -> t -> t.
  Parameter zero : t.
@@ -71,10 +73,12 @@ Module Type ZType.
  Parameter lxor : t -> t -> t.
  Parameter div2 : t -> t.
 
- Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
- Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
- Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
- Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
+ Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]).
+ Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]).
+ Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]).
+ Parameter spec_min : forall x y, [min x y] = Z.min [x] [y].
+ Parameter spec_max : forall x y, [max x y] = Z.max [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
  Parameter spec_2: [two] = 2.
@@ -89,27 +93,27 @@ Module Type ZType.
  Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
- Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
+ Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
+ Parameter spec_log2: forall x, [log2 x] = Z.log2 [x].
  Parameter spec_div_eucl: forall x y,
-   let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+   let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
  Parameter spec_quot: forall x y, [quot x y] = [x] ÷ [y].
- Parameter spec_rem: forall x y, [rem x y] = Zrem [x] [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
- Parameter spec_abs : forall x, [abs x] = Zabs [x].
- Parameter spec_even : forall x, even x = Zeven_bool [x].
- Parameter spec_odd : forall x, odd x = Zodd_bool [x].
- Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
- Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
- Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
- Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
- Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
- Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
- Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
+ Parameter spec_rem: forall x y, [rem x y] = Z.rem [x] [y].
+ Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
+ Parameter spec_sgn : forall x, [sgn x] = Z.sgn [x].
+ Parameter spec_abs : forall x, [abs x] = Z.abs [x].
+ Parameter spec_even : forall x, even x = Z.even [x].
+ Parameter spec_odd : forall x, odd x = Z.odd [x].
+ Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Z.div2 [x].
 
 End ZType.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index a055007f4..e3fc512e7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Bool ZArith Nnat ZAxioms ZSig.
+Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
@@ -15,9 +15,9 @@ Module ZTypeIsZAxioms (Import Z : ZType').
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
- spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot spec_rem
- spec_testbit spec_shiftl spec_shiftr
+ spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min
+ spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd
+ spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr
  spec_land spec_lor spec_ldiff spec_lxor spec_div2
  : zsimpl.
 
@@ -138,36 +138,66 @@ Qed.
 
 (** Order *)
 
-Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
+Lemma eqb_eq x y : eqb x y = true <-> x == y.
 Proof.
- intros. zify. destruct (Zcompare_spec [x] [y]); auto.
+ zify. apply Z.eqb_eq.
 Qed.
 
-Definition eqb := eq_bool.
+Lemma leb_le x y : leb x y = true <-> x <= y.
+Proof.
+ zify. apply Z.leb_le.
+Qed.
+
+Lemma ltb_lt x y : ltb x y = true <-> x < y.
+Proof.
+ zify. apply Z.ltb_lt.
+Qed.
+
+Lemma compare_eq_iff n m : compare n m = Eq <-> n == m.
+Proof.
+ intros. zify. apply Z.compare_eq_iff.
+Qed.
+
+Lemma compare_lt_iff n m : compare n m = Lt <-> n < m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
+
+Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
 
-Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Lemma compare_antisym n m : compare m n = CompOpp (compare n m).
 Proof.
- intros. zify. symmetry. apply Zeq_is_eq_bool.
+ intros. zify. apply Z.compare_antisym.
 Qed.
 
+Include BoolOrderFacts Z Z Z [no inline].
+
 Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
-intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
 Proof.
-intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
 Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Theorem lt_irrefl : forall n, ~ n < n.
+Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
 Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
+Qed.
+
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Proof.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
 Qed.
 
 Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
@@ -491,5 +521,5 @@ Qed.
 End ZTypeIsZAxioms.
 
 Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
+ <: ZAxiomsSig <: OrderFunctions Z <: HasMinMax Z
  := Z <+ ZTypeIsZAxioms.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 09438628d..45a2cf3e1 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -32,11 +32,11 @@ End NDivSpecific.
 
 (** We now group everything together. *)
 
-Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions
   <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
   <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits.
 
-Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions'
   <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
   <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index d2c93bbfd..b06e42ca2 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -62,6 +62,9 @@ Infix "*" := BigN.mul : bigN_scope.
 Infix "/" := BigN.div : bigN_scope.
 Infix "^" := BigN.pow : bigN_scope.
 Infix "?=" := BigN.compare : bigN_scope.
+Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope.
+Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope.
+Infix "<?" := BigN.ltb (at level 70, no associativity) : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
 Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope.
 Infix "<" := BigN.lt : bigN_scope.
@@ -94,7 +97,7 @@ exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm.
 exact BigN.mul_assoc. exact BigN.mul_add_distr_r.
 Qed.
 
-Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y.
+Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y.
 Proof. now apply BigN.eqb_eq. Qed.
 
 Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
@@ -107,11 +110,11 @@ induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto.
 Qed.
 
 Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
- (fun a b => if BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b).
+ (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
 Proof.
 constructor. unfold id. intros a b.
 BigN.zify.
-generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+case Z.eqb_spec.
 BigN.zify. auto with zarith.
 intros NEQ.
 generalize (BigN.spec_div_eucl a b).
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 23cfec5e9..aabbf87f2 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -301,20 +301,48 @@ Module Make (W0:CyclicType) <: NType.
   intros. subst. apply Zcompare_antisym.
  Qed.
 
- Definition eq_bool (x y : t) : bool :=
+ Definition eqb (x y : t) : bool :=
   match compare x y with
   | Eq => true
   | _  => false
   end.
 
- Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y].
+ Theorem spec_eqb x y : eqb x y = Z.eqb [x] [y].
  Proof.
- intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity.
+ apply eq_iff_eq_true.
+ unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare.
+ split; [now destruct Z.compare | now intros ->].
  Qed.
 
  Definition lt (n m : t) := [n] < [m].
  Definition le (n m : t) := [n] <= [m].
 
+ Definition ltb (x y : t) : bool :=
+  match compare x y with
+  | Lt => true
+  | _  => false
+  end.
+
+ Theorem spec_ltb x y : ltb x y = Z.ltb [x] [y].
+ Proof.
+ apply eq_iff_eq_true.
+ rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare.
+ split; [now destruct Z.compare | now intros ->].
+ Qed.
+
+ Definition leb (x y : t) : bool :=
+  match compare x y with
+  | Gt => false
+  | _  => true
+  end.
+
+ Theorem spec_leb x y : leb x y = Z.leb [x] [y].
+ Proof.
+ apply eq_iff_eq_true.
+ rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
+ destruct Z.compare; split; try easy. now destruct 1.
+ Qed.
+
  Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
  Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end.
 
@@ -560,7 +588,7 @@ Module Make (W0:CyclicType) <: NType.
  (** * General Division *)
 
  Definition div_eucl (x y : t) : t * t :=
-  if eq_bool y zero then (zero,zero) else
+  if eqb y zero then (zero,zero) else
   match compare x y with
   | Eq => (one, zero)
   | Lt => (zero, x)
@@ -572,8 +600,8 @@ Module Make (W0:CyclicType) <: NType.
       ([q], [r]) = Zdiv_eucl [x] [y].
  Proof.
  intros x y. unfold div_eucl.
- rewrite spec_eq_bool, spec_compare, spec_0.
- generalize (Zeq_bool_if [y] 0); case Zeq_bool.
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
  intros ->. rewrite spec_0. destruct [x]; auto.
  intros H'.
  assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
@@ -685,7 +713,7 @@ Module Make (W0:CyclicType) <: NType.
  (** * General Modulo *)
 
  Definition modulo (x y : t) : t :=
-  if eq_bool y zero then zero else
+  if eqb y zero then zero else
   match compare x y with
   | Eq => zero
   | Lt => x
@@ -696,8 +724,8 @@ Module Make (W0:CyclicType) <: NType.
    forall x y, [modulo x y] = [x] mod [y].
  Proof.
  intros x y. unfold modulo.
- rewrite spec_eq_bool, spec_compare, spec_0.
- generalize (Zeq_bool_if [y] 0). case Zeq_bool.
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
  intros ->; rewrite spec_0. destruct [x]; auto.
  intro H'.
  assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
@@ -1157,16 +1185,16 @@ Module Make (W0:CyclicType) <: NType.
 
  Definition log2 : t -> t := Eval red_t in
    let log2 := iter_t log2n in
-   fun x => if eq_bool x zero then zero else log2 x.
+   fun x => if eqb x zero then zero else log2 x.
 
  Lemma log2_fold :
-   log2 = fun x => if eq_bool x zero then zero else iter_t log2n x.
+   log2 = fun x => if eqb x zero then zero else iter_t log2n x.
  Proof. red_t; reflexivity. Qed.
 
  Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0.
  Proof.
  intros x H. rewrite log2_fold.
- rewrite spec_eq_bool, H. rewrite spec_0. simpl. exact spec_0.
+ rewrite spec_eqb, H. rewrite spec_0. simpl. exact spec_0.
  Qed.
 
  Lemma head0_zdigits : forall n (x : dom_t n),
@@ -1193,8 +1221,8 @@ Module Make (W0:CyclicType) <: NType.
    2^[log2 x] <= [x] < 2^([log2 x]+1).
  Proof.
  intros x H. rewrite log2_fold.
- rewrite spec_eq_bool. rewrite spec_0.
- generalize (Zeq_bool_if [x] 0). destruct Zeq_bool.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
  auto with zarith.
  clear H.
  destr_t x as (n,x). intros H.
@@ -1229,8 +1257,8 @@ Module Make (W0:CyclicType) <: NType.
    [log2 x] = Zpos (digits x) - [head0 x] - 1.
  Proof.
  intros. rewrite log2_fold.
- rewrite spec_eq_bool. rewrite spec_0.
- generalize (Zeq_bool_if [x] 0). destruct Zeq_bool.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
  auto with zarith.
  intros _. revert H. rewrite digits_fold, head0_fold. destr_t x as (n,x).
  rewrite ZnZ.spec_sub_carry.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0cf9ae441..8a26ec6e3 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -14,6 +14,31 @@ Require Import
 
 (** Functions not already defined *)
 
+Fixpoint leb n m :=
+  match n, m with
+    | O, _ => true
+    | _, O => false
+    | S n', S m' => leb n' m'
+  end.
+
+Definition ltb n m := leb (S n) m.
+
+Infix "<=?" := leb (at level 70) : nat_scope.
+Infix "<?" := ltb (at level 70) : nat_scope.
+
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
+Proof.
+ revert m.
+ induction n. split; auto with arith.
+ destruct m; simpl. now split.
+ rewrite IHn. split; auto with arith.
+Qed.
+
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
+Proof.
+ unfold ltb, lt. apply leb_le.
+Qed.
+
 Fixpoint pow n m :=
   match m with
     | O => 1
@@ -681,6 +706,8 @@ Definition sub := minus.
 Definition mul := mult.
 Definition lt := lt.
 Definition le := le.
+Definition ltb := ltb.
+Definition leb := leb.
 
 Definition min := min.
 Definition max := max.
@@ -692,6 +719,8 @@ Definition min_r := min_r.
 Definition eqb_eq := beq_nat_true_iff.
 Definition compare_spec := nat_compare_spec.
 Definition eq_dec := eq_nat_dec.
+Definition leb_le := leb_le.
+Definition ltb_lt := ltb_lt.
 
 Definition Even := Even.
 Definition Odd := Odd.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index f186c55b4..662648432 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Znumtheory.
+Require Import BinInt.
 
 Open Scope Z_scope.
 
@@ -35,7 +35,9 @@ Module Type NType.
  Definition le n m := [n] <= [m].
 
  Parameter compare : t -> t -> comparison.
- Parameter eq_bool : t -> t -> bool.
+ Parameter eqb : t -> t -> bool.
+ Parameter ltb : t -> t -> bool.
+ Parameter leb : t -> t -> bool.
  Parameter max : t -> t -> t.
  Parameter min : t -> t -> t.
  Parameter zero : t.
@@ -67,39 +69,41 @@ Module Type NType.
  Parameter lxor : t -> t -> t.
  Parameter div2 : t -> t.
 
- Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
- Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
- Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
- Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
+ Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]).
+ Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]).
+ Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]).
+ Parameter spec_max : forall x y, [max x y] = Z.max [x] [y].
+ Parameter spec_min : forall x y, [min x y] = Z.min [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
  Parameter spec_2: [two] = 2.
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
- Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
- Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]).
+ Parameter spec_pred: forall x, [pred x] = Z.max 0 ([x] - 1).
+ Parameter spec_sub: forall x y, [sub x y] = Z.max 0 ([x] - [y]).
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
  Parameter spec_square: forall x, [square x] = [x] *  [x].
  Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
- Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
+ Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
+ Parameter spec_log2: forall x, [log2 x] = Z.log2 [x].
  Parameter spec_div_eucl: forall x y,
-  let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+  let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_even: forall x, even x = Zeven_bool [x].
- Parameter spec_odd: forall x, odd x = Zodd_bool [x].
- Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
- Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
- Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
- Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
- Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
- Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
- Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
+ Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
+ Parameter spec_even: forall x, even x = Z.even [x].
+ Parameter spec_odd: forall x, odd x = Z.odd [x].
+ Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Z.div2 [x].
 
 End NType.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 84682820d..878e46fea 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith Nnat Ndigits NAxioms NDiv NSig.
+Require Import ZArith OrdersFacts Nnat Ndigits NAxioms NDiv NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 
@@ -15,8 +15,8 @@ Module NTypeIsNAxioms (Import N : NType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
- spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt
- spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
+ spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
+ spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
  spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
  spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
  : nsimpl.
@@ -126,36 +126,66 @@ Qed.
 
 (** Order *)
 
-Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
+Lemma eqb_eq x y : eqb x y = true <-> x == y.
 Proof.
- intros. zify. destruct (Zcompare_spec [x] [y]); auto.
+ zify. apply Z.eqb_eq.
 Qed.
 
-Definition eqb := eq_bool.
+Lemma leb_le x y : leb x y = true <-> x <= y.
+Proof.
+ zify. apply Z.leb_le.
+Qed.
+
+Lemma ltb_lt x y : ltb x y = true <-> x < y.
+Proof.
+ zify. apply Z.ltb_lt.
+Qed.
+
+Lemma compare_eq_iff n m : compare n m = Eq <-> n == m.
+Proof.
+ intros. zify. apply Z.compare_eq_iff.
+Qed.
+
+Lemma compare_lt_iff n m : compare n m = Lt <-> n < m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
+
+Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
 
-Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Lemma compare_antisym n m : compare m n = CompOpp (compare n m).
 Proof.
- intros. zify. symmetry. apply Zeq_is_eq_bool.
+ intros. zify. apply Z.compare_antisym.
 Qed.
 
+Include BoolOrderFacts N N N [no inline].
+
 Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
-intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
 Proof.
-intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
 Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
 Qed.
 
-Theorem lt_irrefl : forall n, ~ n < n.
+Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
 Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
+Qed.
+
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Proof.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
 Qed.
 
 Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
@@ -474,5 +504,5 @@ Qed.
 End NTypeIsNAxioms.
 
 Module NType_NAxioms (N : NType)
- <: NAxiomsSig <: HasCompare N <: HasEqBool N <: HasMinMax N
+ <: NAxiomsSig <: OrderFunctions N <: HasMinMax N
  := N <+ NTypeIsNAxioms.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 75a548ca9..d4db2c66d 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -57,7 +57,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Definition to_Q (q: t) :=
  match q with
    | Qz x => Z.to_Z x # 1
-   | Qq x y => if N.eq_bool y N.zero then 0
+   | Qq x y => if N.eqb y N.zero then 0
                else Z.to_Z x # Z2P (N.to_Z y)
  end.
 
@@ -79,15 +79,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 *)
  Ltac destr_eqb :=
   match goal with
-   | |- context [Z.eq_bool ?x ?y] =>
-     rewrite (Z.spec_eq_bool x y);
-     generalize (Zeq_bool_if (Z.to_Z x) (Z.to_Z y));
-     case (Zeq_bool (Z.to_Z x) (Z.to_Z y));
+   | |- context [Z.eqb ?x ?y] =>
+     rewrite (Z.spec_eqb x y);
+     case (Z.eqb_spec (Z.to_Z x) (Z.to_Z y));
      destr_eqb
-   | |- context [N.eq_bool ?x ?y] =>
-     rewrite (N.spec_eq_bool x y);
-     generalize (Zeq_bool_if (N.to_Z x) (N.to_Z y));
-     case (Zeq_bool (N.to_Z x) (N.to_Z y));
+   | |- context [N.eqb ?x ?y] =>
+     rewrite (N.spec_eqb x y);
+     case (Z.eqb_spec (N.to_Z x) (N.to_Z y));
      [ | let H:=fresh "H" in
          try (intro H;generalize (N_to_Z_pos _ H); clear H)];
      destr_eqb
@@ -145,13 +143,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   match x, y with
   | Qz zx, Qz zy => Z.compare zx zy
   | Qz zx, Qq ny dy =>
-    if N.eq_bool dy N.zero then Z.compare zx Z.zero
+    if N.eqb dy N.zero then Z.compare zx Z.zero
     else Z.compare (Z.mul zx (Z_of_N dy)) ny
   | Qq nx dx, Qz zy =>
-    if N.eq_bool dx N.zero then Z.compare Z.zero zy
+    if N.eqb dx N.zero then Z.compare Z.zero zy
     else Z.compare nx (Z.mul zy (Z_of_N dx))
   | Qq nx dx, Qq ny dy =>
-    match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
+    match N.eqb dx N.zero, N.eqb dy N.zero with
     | true, true => Eq
     | true, false => Z.compare Z.zero ny
     | false, true => Z.compare nx Z.zero
@@ -301,15 +299,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
     match y with
     | Qz zy => Qz (Z.add zx zy)
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if N.eqb dy N.zero then x
       else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y
+    if N.eqb dx N.zero then y
     else match y with
     | Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if N.eqb dy N.zero then x
       else
        let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
        let d := N.mul dx dy in
@@ -333,15 +331,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
     match y with
     | Qz zy => Qz (Z.add zx zy)
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if N.eqb dy N.zero then x
       else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y
+    if N.eqb dx N.zero then y
     else match y with
     | Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
-      if N.eq_bool dy N.zero then x
+      if N.eqb dy N.zero then x
       else
        let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
        let d := N.mul dx dy in
@@ -378,8 +376,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros [z | x y]; simpl.
  rewrite Z.spec_opp; auto.
- match goal with  |- context[N.eq_bool ?X ?Y] =>
-  generalize (N.spec_eq_bool X Y); case N.eq_bool
+ match goal with  |- context[N.eqb ?X ?Y] =>
+  generalize (N.spec_eqb X Y); case N.eqb
  end; auto; rewrite N.spec_0.
  rewrite Z.spec_opp; auto.
  Qed.
@@ -429,26 +427,29 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   | Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy)
   end.
 
+ Ltac nsubst :=
+  match goal with E : N.to_Z _ = _ |- _ => rewrite E in * end.
+
  Theorem spec_mul : forall x y, [mul x y] == [x] * [y].
  Proof.
  intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl.
  rewrite Pmult_1_r, Z2P_correct; auto.
  destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
- rewrite H0 in H1; auto with zarith.
- rewrite H0 in H1; auto with zarith.
- rewrite H in H1; nzsimpl; auto with zarith.
+ nsubst; auto with zarith.
+ nsubst; auto with zarith.
+ nsubst; nzsimpl; auto with zarith.
  rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
  Qed.
 
  Definition norm_denum n d :=
-  if N.eq_bool d N.one then Qz n else Qq n d.
+  if N.eqb d N.one then Qz n else Qq n d.
 
  Lemma spec_norm_denum : forall n d,
   [norm_denum n d] == [Qq n d].
  Proof.
  unfold norm_denum; intros; simpl; qsimpl.
  congruence.
- rewrite H0 in *; auto with zarith.
+ nsubst; auto with zarith.
  Qed.
 
  Definition irred n d :=
@@ -528,7 +529,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Qed.
 
  Definition mul_norm_Qz_Qq z n d :=
-   if Z.eq_bool z Z.zero then zero
+   if Z.eqb z Z.zero then zero
    else
     let gcd := N.gcd (Zabs_N z) d in
     match N.compare gcd N.one with
@@ -561,7 +562,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_norm_denum.
  qsimpl.
  rewrite Zdiv_gcd_zero in GT; auto with zarith.
- rewrite H in *. rewrite Zdiv_0_l in *; discriminate.
+ nsubst. rewrite Zdiv_0_l in *; discriminate.
  rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc.
  rewrite Zgcd_div_swap0; try romega.
  ring.
@@ -637,13 +638,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_norm_denum.
  qsimpl.
 
- destruct (Zmult_integral _ _ H0) as [Eq|Eq].
+ match goal with E : (_ * _ = 0)%Z |- _ =>
+  destruct (Zmult_integral _ _ E) as [Eq|Eq] end.
  rewrite Eq in *; simpl in *.
  rewrite <- Hg2' in *; auto with zarith.
  rewrite Eq in *; simpl in *.
  rewrite <- Hg2 in *; auto with zarith.
 
- destruct (Zmult_integral _ _ H) as [Eq|Eq].
+ match goal with E : (_ * _ = 0)%Z |- _ =>
+  destruct (Zmult_integral _ _ E) as [Eq|Eq] end.
  rewrite Hz' in Eq; rewrite Eq in *; auto with zarith.
  rewrite Hz in Eq; rewrite Eq in *; auto with zarith.
 
@@ -691,13 +694,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
- destruct (rel_prime_bezout _ _ H4) as [u v Huv].
+ destruct (rel_prime_bezout (Z.to_Z ny) (N.to_Z dy)) as [u v Huv]; trivial.
  apply Bezout_intro with (u*g')%Z (v*g)%Z.
  rewrite <- Huv, <- Hg1', <- Hg2. ring.
 
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
- destruct (rel_prime_bezout _ _ H3) as [u v Huv].
+ destruct (rel_prime_bezout (Z.to_Z nx) (N.to_Z dx)) as [u v Huv]; trivial.
  apply Bezout_intro with (u*g)%Z (v*g')%Z.
  rewrite <- Huv, <- Hg2', <- Hg1. ring.
  Qed.
@@ -755,10 +758,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destr_eqb; nzsimpl; intros.
  intros; rewrite Zabs_eq in *; romega.
  intros; rewrite Zabs_eq in *; romega.
- clear H1.
- rewrite H0.
- compute; auto.
- clear H1.
+ nsubst; compute; auto.
  set (n':=Z.to_Z n) in *; clearbody n'.
  rewrite Zabs_eq by romega.
  red; simpl.
@@ -770,9 +770,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destr_eqb; nzsimpl; intros.
  intros; rewrite Zabs_non_eq in *; romega.
  intros; rewrite Zabs_non_eq in *; romega.
- clear H1.
- red; nzsimpl; rewrite H0; compute; auto.
- clear H1.
+ nsubst; compute; auto.
  set (n':=Z.to_Z n) in *; clearbody n'.
  red; simpl; nzsimpl.
  rewrite Zabs_non_eq by romega.
@@ -791,7 +789,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
          | Gt => Qq Z.minus_one (Zabs_N z)
        end
      | Qq n d =>
-       if N.eq_bool d N.zero then zero else
+       if N.eqb d N.zero then zero else
        match Z.compare Z.zero n with
          | Eq => zero
          | Lt =>
@@ -928,9 +926,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destr_eqb; nzsimpl; intros.
  apply Qeq_refl.
  rewrite N.spec_square in *; nzsimpl.
- elim (Zmult_integral _ _ H0); romega.
- rewrite N.spec_square in *; nzsimpl.
- rewrite H in H0; romega.
+ match goal with E : (_ * _ = 0)%Z |- _ =>
+  elim (Zmult_integral _ _ E); romega end.
+ rewrite N.spec_square in *; nzsimpl; nsubst; romega.
  rewrite Z.spec_square, N.spec_square.
  red; simpl.
  rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto.
@@ -961,8 +959,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (0 < N.to_Z d ^ ' p)%Z by
   (apply Zpower_gt_0; auto with zarith).
  romega.
- rewrite N.spec_pow_pos, H in *.
- rewrite Zpower_0_l in H0; [romega|discriminate].
+ exfalso.
+ rewrite N.spec_pow_pos in *. nsubst.
+ rewrite Zpower_0_l in *; [romega|discriminate].
  rewrite Qpower_decomp.
  red; simpl; do 3 f_equal.
  rewrite Z2P_correct by (generalize (N.spec_pos d); romega).
@@ -981,8 +980,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  revert H.
  unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl.
  destr_eqb; nzsimpl; simpl; intros.
- rewrite N.spec_pow_pos in H0.
- rewrite H, Zpower_0_l in *; [romega|discriminate].
+ exfalso.
+ rewrite N.spec_pow_pos in *. nsubst.
+ rewrite Zpower_0_l in *; [romega|discriminate].
  rewrite Z2P_correct in *; auto.
  rewrite N.spec_pow_pos, Z.spec_pow_pos; auto.
  rewrite Zgcd_1_rel_prime in *.