Arith: full integration of the "Numbers" modular framework

 - The earlier proof-of-concept file NPeano (which instantiates
   the "Numbers" framework for nat) becomes now the entry point
   in the Arith lib, and gets renamed PeanoNat. It still provides
   an inner module "Nat" which sums up everything about type nat
   (functions, predicates and properties of them).
   This inner module Nat is usable as soon as you Require Import Arith,
   or just Arith_base, or simply PeanoNat.

 - Definitions of operations over type nat are now grouped in a new
   file Init/Nat.v. This file is meant to be used without "Import",
   hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
   starts (but no proofs about them).

 - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
   are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
   where here Nat is Init/Nat.v).

 - This Coq.Init.Nat module (with only pure definitions) is Include'd
   in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
   sometimes instead of just Nat (for instance when doing "Print plus").
   Normally it should be ok to just ignore these "Init" since
   Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
   it's possible to get rid of these "Init" prefixes.

 - Concerning predicates, orders le and lt are still defined in Init/Peano.v,
   with their notations "<=" and "<". Properties in PeanoNat.Nat directly
   refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
   also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
   we cannot yet include an Inductive to implement a Parameter), but these
   aliased predicates won't probably be very convenient to use.

 - Technical remark: I've split the previous property functor NProp in
   two parts (NBasicProp and NExtraProp), it helps a lot for building
   PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:

   Module Nat.
     Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
     ... (** proofs of specifications for basic ops such as + * - *)
     Include NBasicProp. (** generic properties of these basic ops *)
     ... (** proofs of specifications for advanced ops (pow sqrt log2...)
             that may rely on proofs for + * - *)
     Include NExtraProp. (** all remaining properties *)
   End Nat.

- All other files in directory Arith are now taking advantage of PeanoNat :
  they are now filled with compatibility notations (when earlier lemmas
  have exact counterpart in the Nat module) or lemmas with one-line proofs
  based on the Nat module. All hints for database "arith" remain declared
  in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
  files are still Require'd (or not) by Arith.v, just as before.

- Compatibility should be almost complete. For instance in the stdlib,
  the only adaptations were due to .ml code referring to some Coq constant
  name such as Coq.Init.Peano.pred, which doesn't live well with the
  new compatibility notations.

4 files changed, 178 insertions, 211 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 452e3d148..673eed6bb 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -8,7 +8,7 @@
 (************************************************************************)
 
 Require Export BinNums BinPos Pnat.
-Require Import BinNat Bool Plus Mult Equalities GenericMinMax
+Require Import BinNat Bool Equalities GenericMinMax
  OrdersFacts ZAxioms ZProperties.
 Require BinIntDef.
 
@@ -73,6 +73,23 @@ Proof.
  decide equality; apply Pos.eq_dec.
 Defined.
 
+(** * Proofs of morphisms, obvious since eq is Leibniz *)
+
+Local Obligation Tactic := simpl_relation.
+Program Definition succ_wd : Proper (eq==>eq) succ := _.
+Program Definition pred_wd : Proper (eq==>eq) pred := _.
+Program Definition opp_wd : Proper (eq==>eq) opp := _.
+Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
+Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
+Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
+Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
+Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
+Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
+Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
+Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
+Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
+Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+
 (** * Properties of [pos_sub] *)
 
 (** [pos_sub] can be written in term of positive comparison
@@ -138,15 +155,23 @@ Qed.
 
 Module Import Private_BootStrap.
 
-(** * Properties of addition *)
-
-(** ** Zero is neutral for addition *)
+(** ** Operations and constants *)
 
 Lemma add_0_r n : n + 0 = n.
 Proof.
  now destruct n.
 Qed.
 
+Lemma mul_0_r n : n * 0 = 0.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma mul_1_l n : 1 * n = n.
+Proof.
+ now destruct n.
+Qed.
+
 (** ** Addition is commutative *)
 
 Lemma add_comm n m : n + m = m + n.
@@ -196,28 +221,25 @@ Proof.
    symmetry. now apply Pos.add_sub_assoc.
 Qed.
 
-Lemma add_assoc n m p : n + (m + p) = n + m + p.
+Local Arguments add !x !y.
+
+Lemma add_assoc_pos p n m : pos p + (n + m) = pos p + n + m.
 Proof.
- assert (AUX : forall x y z, pos x + (y + z) = pos x + y + z).
- { intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial.
-   - simpl. now rewrite Pos.add_assoc.
-   - simpl (_ + neg _). symmetry. apply pos_sub_add.
-   - simpl (neg _ + _); simpl (_ + neg _).
-     now rewrite (add_comm _ (pos _)), <- 2 pos_sub_add, Pos.add_comm.
-   - apply opp_inj. rewrite !opp_add_distr. simpl opp.
-     simpl (neg _ + _); simpl (_ + neg _).
-     rewrite add_comm, Pos.add_comm. apply pos_sub_add. }
- destruct n.
- - trivial.
- - apply AUX.
- - apply opp_inj. rewrite !opp_add_distr. simpl opp. apply AUX.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial.
+ - now rewrite Pos.add_assoc.
+ - symmetry. apply pos_sub_add.
+ - symmetry. apply add_0_r.
+ - now rewrite <- pos_sub_add, add_comm, <- pos_sub_add, Pos.add_comm.
+ - apply opp_inj. rewrite !opp_add_distr, !pos_sub_opp.
+   rewrite add_comm, Pos.add_comm. apply pos_sub_add.
 Qed.
 
-(** ** Subtraction and successor *)
-
-Lemma sub_succ_l n m : succ n - m = succ (n - m).
+Lemma add_assoc n m p : n + (m + p) = n + m + p.
 Proof.
- unfold sub, succ. now rewrite <- 2 add_assoc, (add_comm 1).
+ destruct n.
+ - trivial.
+ - apply add_assoc_pos.
+ - apply opp_inj. rewrite !opp_add_distr. simpl. apply add_assoc_pos.
 Qed.
 
 (** ** Opposite is inverse for addition *)
@@ -227,132 +249,34 @@ Proof.
  destruct n; simpl; trivial; now rewrite pos_sub_diag.
 Qed.
 
-Lemma add_opp_diag_l n : - n + n = 0.
-Proof.
- rewrite add_comm. apply add_opp_diag_r.
-Qed.
-
-(** ** Commutativity of multiplication *)
-
-Lemma mul_comm n m : n * m = m * n.
-Proof.
- destruct n, m; simpl; trivial; f_equal; apply Pos.mul_comm.
-Qed.
-
-(** ** Associativity of multiplication *)
-
-Lemma mul_assoc n m p : n * (m * p) = n * m * p.
-Proof.
- destruct n, m, p; simpl; trivial; f_equal; apply Pos.mul_assoc.
-Qed.
-
-(** Multiplication and constants *)
-
-Lemma mul_1_l n : 1 * n = n.
-Proof.
- now destruct n.
-Qed.
-
-Lemma mul_1_r n : n * 1 = n.
-Proof.
- destruct n; simpl; now rewrite ?Pos.mul_1_r.
-Qed.
-
 (** ** Multiplication and Opposite *)
 
-Lemma mul_opp_l n m : - n * m = - (n * m).
-Proof.
- now destruct n, m.
-Qed.
-
 Lemma mul_opp_r n m : n * - m = - (n * m).
 Proof.
  now destruct n, m.
 Qed.
 
-Lemma mul_opp_opp n m : - n * - m = n * m.
-Proof.
- now destruct n, m.
-Qed.
-
-Lemma mul_opp_comm n m : - n * m = n * - m.
-Proof.
- now destruct n, m.
-Qed.
-
 (** ** Distributivity of multiplication over addition *)
 
 Lemma mul_add_distr_pos (p:positive) n m :
- pos p * (n + m) = pos p * n + pos p * m.
-Proof.
- destruct n as [|n|n], m as [|m|m]; simpl; trivial;
- rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec;
- intros; now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l.
-Qed.
-
-Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
+ (n + m) * pos p = n * pos p + m * pos p.
 Proof.
- destruct n as [|n|n]. trivial.
- apply mul_add_distr_pos.
- change (neg n) with (- pos n).
- rewrite !mul_opp_l, <- opp_add_distr. f_equal.
- apply mul_add_distr_pos.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial.
+ - now rewrite Pos.mul_add_distr_r.
+ - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec;
+   simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r.
+ - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec;
+   simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r.
+ - now rewrite Pos.mul_add_distr_r.
 Qed.
 
 Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
 Proof.
- rewrite !(mul_comm _ p). apply mul_add_distr_l.
-Qed.
-
-(** ** Basic properties of divisibility *)
-
-Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive.
-Proof.
- split.
- intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto.
- intros (r,H). exists (pos r); simpl; now f_equal.
-Qed.
-
-Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p).
-Proof.
- split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H.
-Qed.
-
-Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n).
-Proof.
- split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r.
-Qed.
-
-(** ** Conversions between [Z.testbit] and [N.testbit] *)
-
-Lemma testbit_of_N a n :
- testbit (of_N a) (of_N n) = N.testbit a n.
-Proof.
- destruct a as [|a], n; simpl; trivial. now destruct a.
-Qed.
-
-Lemma testbit_of_N' a n : 0<=n ->
- testbit (of_N a) n = N.testbit a (to_N n).
-Proof.
- intro Hn. rewrite <- testbit_of_N. f_equal.
- destruct n; trivial; now destruct Hn.
-Qed.
-
-Lemma testbit_Zpos a n : 0<=n ->
- testbit (pos a) n = N.testbit (N.pos a) (to_N n).
-Proof.
- intro Hn. now rewrite <- testbit_of_N'.
-Qed.
-
-Lemma testbit_Zneg a n : 0<=n ->
- testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)).
-Proof.
- intro Hn.
- rewrite <- testbit_of_N' by trivial.
- destruct n as [ |n|n];
-  [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn].
- unfold testbit.
- now destruct a as [|[ | | ]| ].
+ destruct p as [|p|p].
+ - now rewrite !mul_0_r.
+ - apply mul_add_distr_pos.
+ - apply opp_inj. rewrite opp_add_distr, <- !mul_opp_r.
+   apply mul_add_distr_pos.
 Qed.
 
 End Private_BootStrap.
@@ -397,6 +321,8 @@ Qed.
 
 (** ** Specification of successor and predecessor *)
 
+Local Arguments pos_sub : simpl nomatch.
+
 Lemma succ_pred n : succ (pred n) = n.
 Proof.
  unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r.
@@ -511,6 +437,45 @@ Proof.
  rewrite (compare_antisym n m). case compare_spec; intuition.
 Qed.
 
+(** ** Induction principles based on successor / predecessor *)
+
+Lemma peano_ind (P : Z -> Prop) :
+  P 0 ->
+  (forall x, P x -> P (succ x)) ->
+  (forall x, P x -> P (pred x)) ->
+  forall z, P z.
+Proof.
+ intros H0 Hs Hp z; destruct z.
+ assumption.
+ induction p using Pos.peano_ind.
+  now apply (Hs 0).
+  rewrite <- Pos.add_1_r.
+  now apply (Hs (pos p)).
+ induction p using Pos.peano_ind.
+  now apply (Hp 0).
+  rewrite <- Pos.add_1_r.
+  now apply (Hp (neg p)).
+Qed.
+
+Lemma bi_induction (P : Z -> Prop) :
+  Proper (eq ==> iff) P ->
+  P 0 ->
+  (forall x, P x <-> P (succ x)) ->
+  forall z, P z.
+Proof.
+ intros _ H0 Hs. induction z using peano_ind.
+ assumption.
+ now apply -> Hs.
+ apply Hs. now rewrite succ_pred.
+Qed.
+
+(** We can now derive all properties of basic functions and orders,
+    and use these properties for proving the specs of more advanced
+    functions. *)
+
+Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+
+
 (** ** Specification of absolute value *)
 
 Lemma abs_eq n : 0 <= n -> abs n = n.
@@ -693,7 +658,7 @@ Lemma div_eucl_eq a b : b<>0 ->
 Proof.
  destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial;
   (now destruct 1) || intros _;
-  generalize (pos_div_eucl_eq a (pos b) (eq_refl _));
+  generalize (pos_div_eucl_eq a (pos b) Logic.eq_refl);
   destruct pos_div_eucl as (q,r); rewrite mul_comm.
  - (* pos pos *)
    trivial.
@@ -756,7 +721,7 @@ Proof.
  destruct a as [|a|a]; unfold modulo, div_eucl.
  now split.
  now apply pos_div_eucl_bound.
- generalize (pos_div_eucl_bound a (pos b) (eq_refl _)).
+ generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl).
  destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
  destruct r as [|r|r]; (now destruct Hr) || clear Hr.
  now split.
@@ -773,7 +738,7 @@ Proof.
  destruct b as [|b|b]; try easy; intros _.
  destruct a as [|a|a]; unfold modulo, div_eucl.
  now split.
- generalize (pos_div_eucl_bound a (pos b) (eq_refl _)).
+ generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl).
  destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
  destruct r as [|r|r]; (now destruct Hr) || clear Hr.
  now split.
@@ -783,7 +748,7 @@ Proof.
  change (neg b - neg r <= 0). unfold le, lt in *.
   rewrite <- compare_sub. simpl in *.
   now rewrite <- Pos.compare_antisym, Hr'.
- generalize (pos_div_eucl_bound a (pos b) (eq_refl _)).
+ generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl).
  destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
  split; destruct r; try easy.
   red; simpl; now rewrite <- Pos.compare_antisym.
@@ -839,6 +804,25 @@ Proof. intros _. apply rem_opp_l'. Qed.
 Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b.
 Proof. intros _. apply rem_opp_r'. Qed.
 
+(** ** Extra properties about [divide] *)
+
+Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive.
+Proof.
+ split.
+ intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto.
+ intros (r,H). exists (pos r); simpl; now f_equal.
+Qed.
+
+Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p).
+Proof.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H.
+Qed.
+
+Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n).
+Proof.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r.
+Qed.
+
 (** ** Correctness proofs for gcd *)
 
 Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.
@@ -898,6 +882,38 @@ Proof.
   destruct (Pos.ggcd a b) as (g,(aa,bb)); auto.
 Qed.
 
+(** ** Extra properties about [testbit] *)
+
+Lemma testbit_of_N a n :
+ testbit (of_N a) (of_N n) = N.testbit a n.
+Proof.
+ destruct a as [|a], n; simpl; trivial. now destruct a.
+Qed.
+
+Lemma testbit_of_N' a n : 0<=n ->
+ testbit (of_N a) n = N.testbit a (to_N n).
+Proof.
+ intro Hn. rewrite <- testbit_of_N. f_equal.
+ destruct n; trivial; now destruct Hn.
+Qed.
+
+Lemma testbit_Zpos a n : 0<=n ->
+ testbit (pos a) n = N.testbit (N.pos a) (to_N n).
+Proof.
+ intro Hn. now rewrite <- testbit_of_N'.
+Qed.
+
+Lemma testbit_Zneg a n : 0<=n ->
+ testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)).
+Proof.
+ intro Hn.
+ rewrite <- testbit_of_N' by trivial.
+ destruct n as [ |n|n];
+  [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn].
+ unfold testbit.
+ now destruct a as [|[ | | ]| ].
+Qed.
+
 (** ** Proofs of specifications for bitwise operations *)
 
 Lemma div2_spec a : div2 a = shiftr a 1.
@@ -1103,59 +1119,10 @@ Proof.
  now rewrite N.lxor_spec, xorb_negb_negb.
 Qed.
 
-(** ** Induction principles based on successor / predecessor *)
 
-Lemma peano_ind (P : Z -> Prop) :
-  P 0 ->
-  (forall x, P x -> P (succ x)) ->
-  (forall x, P x -> P (pred x)) ->
-  forall z, P z.
-Proof.
- intros H0 Hs Hp z; destruct z.
- assumption.
- induction p using Pos.peano_ind.
-  now apply (Hs 0).
-  rewrite <- Pos.add_1_r.
-  now apply (Hs (pos p)).
- induction p using Pos.peano_ind.
-  now apply (Hp 0).
-  rewrite <- Pos.add_1_r.
-  now apply (Hp (neg p)).
-Qed.
-
-Lemma bi_induction (P : Z -> Prop) :
-  Proper (eq ==> iff) P ->
-  P 0 ->
-  (forall x, P x <-> P (succ x)) ->
-  forall z, P z.
-Proof.
- intros _ H0 Hs. induction z using peano_ind.
- assumption.
- now apply -> Hs.
- apply Hs. now rewrite succ_pred.
-Qed.
-
-
-(** * Proofs of morphisms, obvious since eq is Leibniz *)
-
-Local Obligation Tactic := simpl_relation.
-Program Definition succ_wd : Proper (eq==>eq) succ := _.
-Program Definition pred_wd : Proper (eq==>eq) pred := _.
-Program Definition opp_wd : Proper (eq==>eq) opp := _.
-Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
-Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
-Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
-Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
-Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
-Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
-Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
-Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
-Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
-Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+(** Generic properties of advanced functions. *)
 
-Include ZProp
- <+ UsualMinMaxLogicalProperties
- <+ UsualMinMaxDecProperties.
+Include ZExtraProp.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -1394,11 +1361,11 @@ Lemma inj_gcd p q : Z.pos (Pos.gcd p q) = Z.gcd (Z.pos p) (Z.pos q).
 Proof. reflexivity. Qed.
 
 Definition inj_divide p q : (Z.pos p|Z.pos q) <-> (p|q)%positive.
-Proof. apply Z.Private_BootStrap.divide_Zpos. Qed.
+Proof. apply Z.divide_Zpos. Qed.
 
 Lemma inj_testbit a n : 0<=n ->
  Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
-Proof. apply Z.Private_BootStrap.testbit_Zpos. Qed.
+Proof. apply Z.testbit_Zpos. Qed.
 
 (** Some results concerning Z.neg *)
 
@@ -1436,14 +1403,14 @@ Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p.
 Proof. reflexivity. Qed.
 
 Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p).
-Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_r. Qed.
+Proof. apply Z.divide_Zpos_Zneg_r. Qed.
 
 Lemma divide_pos_neg_l n p : (Z.pos p|n) <-> (Z.neg p|n).
-Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_l. Qed.
+Proof. apply Z.divide_Zpos_Zneg_l. Qed.
 
 Lemma testbit_neg a n : 0<=n ->
  Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)).
-Proof. apply Z.Private_BootStrap.testbit_Zneg. Qed.
+Proof. apply Z.testbit_Zneg. Qed.
 
 End Pos2Z.
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 27fb21bc7..32993b2c0 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -683,7 +683,7 @@ Arguments Zdiv_eucl_extended : default implicits.
 
 (** * Division and modulo in Z agree with same in nat: *)
 
-Require Import NPeano.
+Require Import PeanoNat.
 
 Lemma div_Zdiv (n m: nat): m <> O ->
   Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 27b7e6a0c..28003bc02 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -271,7 +271,7 @@ Qed.
 
 Lemma inj_testbit a n :
  Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n.
-Proof. apply Z.Private_BootStrap.testbit_of_N. Qed.
+Proof. apply Z.testbit_of_N. Qed.
 
 End N2Z.
 
@@ -426,7 +426,7 @@ Qed.
 
 Lemma inj_testbit a n : 0<=n ->
  Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n).
-Proof. apply Z.Private_BootStrap.testbit_of_N'. Qed.
+Proof. apply Z.testbit_of_N'. Qed.
 
 End Z2N.
 
@@ -637,7 +637,7 @@ Qed.
 
 (** [Z.of_nat] and usual operations *)
 
-Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = nat_compare n m.
+Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = (n ?= m)%nat.
 Proof.
  now rewrite <-!nat_N_Z, N2Z.inj_compare, <- Nat2N.inj_compare.
 Qed.
@@ -690,23 +690,23 @@ Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub.
 Qed.
 
-Lemma inj_pred_max n : Z.of_nat (pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
+Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max.
 Qed.
 
-Lemma inj_pred n : (0<n)%nat -> Z.of_nat (pred n) = Z.pred (Z.of_nat n).
+Lemma inj_pred n : (0<n)%nat -> Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n).
 Proof.
  rewrite nat_compare_lt, Nat2N.inj_compare. intros.
  now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred.
 Qed.
 
-Lemma inj_min n m : Z.of_nat (min n m) = Z.min (Z.of_nat n) (Z.of_nat m).
+Lemma inj_min n m : Z.of_nat (Nat.min n m) = Z.min (Z.of_nat n) (Z.of_nat m).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_min, N2Z.inj_min.
 Qed.
 
-Lemma inj_max n m : Z.of_nat (max n m) = Z.max (Z.of_nat n) (Z.of_nat m).
+Lemma inj_max n m : Z.of_nat (Nat.max n m) = Z.max (Z.of_nat n) (Z.of_nat m).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_max, N2Z.inj_max.
 Qed.
@@ -777,13 +777,13 @@ Proof.
  intros. now rewrite <- !Z_N_nat, Z2N.inj_sub, N2Nat.inj_sub.
 Qed.
 
-Lemma inj_pred n : Z.to_nat (Z.pred n) = pred (Z.to_nat n).
+Lemma inj_pred n : Z.to_nat (Z.pred n) = Nat.pred (Z.to_nat n).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_pred, N2Nat.inj_pred.
 Qed.
 
 Lemma inj_compare n m : 0<=n -> 0<=m ->
- nat_compare (Z.to_nat n) (Z.to_nat m) = (n ?= m).
+ (Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m).
 Proof.
  intros Hn Hm. now rewrite <- Nat2Z.inj_compare, !id.
 Qed.
@@ -798,12 +798,12 @@ Proof.
  intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare.
 Qed.
 
-Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m).
+Lemma inj_min n m : Z.to_nat (Z.min n m) = Nat.min (Z.to_nat n) (Z.to_nat m).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min.
 Qed.
 
-Lemma inj_max n m : Z.to_nat (Z.max n m) = max (Z.to_nat n) (Z.to_nat m).
+Lemma inj_max n m : Z.to_nat (Z.max n m) = Nat.max (Z.to_nat n) (Z.to_nat m).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_max, N2Nat.inj_max.
 Qed.
@@ -876,13 +876,13 @@ Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_sub, N2Nat.inj_sub.
 Qed.
 
-Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = pred (Z.abs_nat n).
+Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_pred, N2Nat.inj_pred.
 Qed.
 
 Lemma inj_compare n m : 0<=n -> 0<=m ->
- nat_compare (Z.abs_nat n) (Z.abs_nat m) = (n ?= m).
+ (Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare.
 Qed.
@@ -898,13 +898,13 @@ Proof.
 Qed.
 
 Lemma inj_min n m : 0<=n -> 0<=m ->
- Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m).
+ Z.abs_nat (Z.min n m) = Nat.min (Z.abs_nat n) (Z.abs_nat m).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_min, N2Nat.inj_min.
 Qed.
 
 Lemma inj_max n m : 0<=n -> 0<=m ->
- Z.abs_nat (Z.max n m) = max (Z.abs_nat n) (Z.abs_nat m).
+ Z.abs_nat (Z.max n m) = Nat.max (Z.abs_nat n) (Z.abs_nat m).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_max, N2Nat.inj_max.
 Qed.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 1da3c7992..485935502 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -25,7 +25,7 @@ Local Open Scope Z_scope.
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *)
 
-Definition Zpower_nat (z:Z) := nat_rect _ 1 (fun _ => Z.mul z).
+Definition Zpower_nat (z:Z)(n:nat) := Nat.iter n (Z.mul z) 1.
 
 Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.
 Proof. reflexivity. Qed.
@@ -255,7 +255,7 @@ Section power_div_with_rest.
   Proof.
    rewrite Pos2Nat.inj_iter, two_power_pos_nat.
    induction (Pos.to_nat p); simpl; trivial.
-   destruct (nat_rect _ _ _ n) as ((q,r),d).
+   destruct (Nat.iter _ _ _) as ((q,r),d).
    unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal.
   Qed.