ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

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

5 files changed, 338 insertions, 468 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 6128b9740..046670f7b 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -76,7 +76,7 @@ Defined.
 
 (** Discrimination principle *)
 
-Definition discr n : { p:positive | n = Npos p } + { n = N0 }.
+Definition discr n : { p:positive | n = pos p } + { n = 0 }.
 Proof.
  destruct n; auto.
  left; exists p; auto.
@@ -87,12 +87,12 @@ Defined.
 Definition binary_rect (P:N -> Type) (f0 : P 0)
   (f2 : forall n, P n -> P (double n))
   (fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n :=
- let P' p := P (Npos p) in
- let f2' p := f2 (Npos p) in
- let fS2' p := fS2 (Npos p) in
+ let P' p := P (pos p) in
+ let f2' p := f2 (pos p) in
+ let fS2' p := fS2 (pos p) in
  match n with
  | 0 => f0
- | Npos p => positive_rect P' fS2' f2' (fS2 0 f0) p
+ | pos p => positive_rect P' fS2' f2' (fS2 0 f0) p
  end.
 
 Definition binary_rec (P:N -> Set) := binary_rect P.
@@ -103,11 +103,11 @@ Definition binary_ind (P:N -> Prop) := binary_rect P.
 Definition peano_rect
   (P : N -> Type) (f0 : P 0)
     (f : forall n : N, P n -> P (succ n)) (n : N) : P n :=
-let P' p := P (Npos p) in
-let f' p := f (Npos p) in
+let P' p := P (pos p) in
+let f' p := f (pos p) in
 match n with
 | 0 => f0
-| Npos p => Pos.peano_rect P' (f 0 f0) f' p
+| pos p => Pos.peano_rect P' (f 0 f0) f' p
 end.
 
 Theorem peano_rect_base P a f : peano_rect P a f 0 = a.
@@ -140,12 +140,12 @@ Qed.
 
 (** Properties of mixed successor and predecessor. *)
 
-Lemma pos_pred_spec p : Pos.pred_N p = pred (Npos p).
+Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p).
 Proof.
  now destruct p.
 Qed.
 
-Lemma succ_pos_spec n : Npos (succ_pos n) = succ n.
+Lemma succ_pos_spec n : pos (succ_pos n) = succ n.
 Proof.
  now destruct n.
 Qed.
@@ -155,7 +155,7 @@ Proof.
  destruct n. trivial. apply Pos.pred_N_succ.
 Qed.
 
-Lemma succ_pos_pred p : succ (Pos.pred_N p) = Npos p.
+Lemma succ_pos_pred p : succ (Pos.pred_N p) = pos p.
 Proof.
  destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double.
 Qed.
@@ -472,7 +472,7 @@ Lemma log2_spec n : 0 < n ->
  2^(log2 n) <= n < 2^(succ (log2 n)).
 Proof.
  destruct n as [|[p|p|]]; discriminate || intros _; simpl; split.
- apply (size_le (Npos p)).
+ apply (size_le (pos p)).
  apply Pos.size_gt.
  apply Pos.size_le.
  apply Pos.size_gt.
@@ -494,7 +494,7 @@ Proof.
  trivial.
  destruct p; simpl; split; try easy.
  intros (m,H). now destruct m.
- now exists (Npos p).
+ now exists (pos p).
  intros (m,H). now destruct m.
 Qed.
 
@@ -504,7 +504,7 @@ Proof.
  split. discriminate.
  intros (m,H). now destruct m.
  destruct p; simpl; split; try easy.
- now exists (Npos p).
+ now exists (pos p).
  intros (m,H). now destruct m.
  now exists 0.
 Qed.
@@ -512,19 +512,19 @@ Qed.
 (** Specification of the euclidean division *)
 
 Theorem pos_div_eucl_spec (a:positive)(b:N) :
-  let (q,r) := pos_div_eucl a b in Npos a = q * b + r.
+  let (q,r) := pos_div_eucl a b in pos a = q * b + r.
 Proof.
   induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.
   (* a~1 *)
   destruct pos_div_eucl as (q,r).
-  change (Npos a~1) with (succ_double (Npos a)).
+  change (pos a~1) with (succ_double (pos a)).
   rewrite IHa, succ_double_add, double_mul.
   case leb_spec; intros H; trivial.
   rewrite succ_double_mul, <- add_assoc. f_equal.
   now rewrite (add_comm b), sub_add.
   (* a~0 *)
   destruct pos_div_eucl as (q,r).
-  change (Npos a~0) with (double (Npos a)).
+  change (pos a~0) with (double (pos a)).
   rewrite IHa, double_add, double_mul.
   case leb_spec; intros H; trivial.
   rewrite succ_double_mul, <- add_assoc. f_equal.
@@ -537,7 +537,7 @@ Theorem div_eucl_spec a b :
  let (q,r) := div_eucl a b in a = b * q + r.
 Proof.
   destruct a as [|a], b as [|b]; unfold div_eucl; trivial.
-  generalize (pos_div_eucl_spec a (Npos b)).
+  generalize (pos_div_eucl_spec a (pos b)).
   destruct pos_div_eucl. now rewrite mul_comm.
 Qed.
 
@@ -664,7 +664,7 @@ Proof.
  destruct (Pos.gcd_greatest p q r) as (u,H).
  exists s. now inversion Hs.
  exists t. now inversion Ht.
- exists (Npos u). simpl; now f_equal.
+ exists (pos u). simpl; now f_equal.
 Qed.
 
 Lemma gcd_nonneg a b : 0 <= gcd a b.
@@ -862,7 +862,7 @@ Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
 
 Theorem bi_induction :
   forall A : N -> Prop, Proper (Logic.eq==>iff) A ->
-    A N0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
+    A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
 Proof.
 intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS.
 Qed.
@@ -1018,7 +1018,7 @@ Notation N_rect := N_rect (only parsing).
 Notation N_rec := N_rec (only parsing).
 Notation N_ind := N_ind (only parsing).
 Notation N0 := N0 (only parsing).
-Notation Npos := Npos (only parsing).
+Notation Npos := N.pos (only parsing).
 
 Notation Ndiscr := N.discr (compat "8.3").
 Notation Ndouble_plus_one := N.succ_double (compat "8.3").
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index b95c9b4bc..76526a5ce 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -19,6 +19,10 @@ Module N.
 
 Definition t := N.
 
+(** ** Nicer name [N.pos] for contructor [Npos] *)
+
+Notation pos := Npos.
+
 (** ** Constants *)
 
 Definition zero := 0.
@@ -30,7 +34,7 @@ Definition two := 2.
 Definition succ_double x :=
   match x with
   | 0 => 1
-  | Npos p => Npos p~1
+  | pos p => pos p~1
   end.
 
 (** ** Operation [x -> 2*x] *)
@@ -38,7 +42,7 @@ Definition succ_double x :=
 Definition double n :=
   match n with
   | 0 => 0
-  | Npos p => Npos p~0
+  | pos p => pos p~0
   end.
 
 (** ** Successor *)
@@ -46,7 +50,7 @@ Definition double n :=
 Definition succ n :=
   match n with
   | 0 => 1
-  | Npos p => Npos (Pos.succ p)
+  | pos p => pos (Pos.succ p)
   end.
 
 (** ** Predecessor *)
@@ -54,15 +58,15 @@ Definition succ n :=
 Definition pred n :=
   match n with
   | 0 => 0
-  | Npos p => Pos.pred_N p
+  | pos p => Pos.pred_N p
   end.
 
 (** ** The successor of a [N] can be seen as a [positive] *)
 
 Definition succ_pos (n : N) : positive :=
  match n with
-   | N0 => 1%positive
-   | Npos p => Pos.succ p
+   | 0 => 1%positive
+   | pos p => Pos.succ p
  end.
 
 (** ** Addition *)
@@ -71,7 +75,7 @@ Definition add n m :=
   match n, m with
   | 0, _ => m
   | _, 0 => n
-  | Npos p, Npos q => Npos (p + q)
+  | pos p, pos q => pos (p + q)
   end.
 
 Infix "+" := add : N_scope.
@@ -82,9 +86,9 @@ Definition sub n m :=
 match n, m with
 | 0, _ => 0
 | n, 0 => n
-| Npos n', Npos m' =>
+| pos n', pos m' =>
   match Pos.sub_mask n' m' with
-  | IsPos p => Npos p
+  | IsPos p => pos p
   | _ => 0
   end
 end.
@@ -97,7 +101,7 @@ Definition mul n m :=
   match n, m with
   | 0, _ => 0
   | _, 0 => 0
-  | Npos p, Npos q => Npos (p * q)
+  | pos p, pos q => pos (p * q)
   end.
 
 Infix "*" := mul : N_scope.
@@ -107,9 +111,9 @@ Infix "*" := mul : N_scope.
 Definition compare n m :=
   match n, m with
   | 0, 0 => Eq
-  | 0, Npos m' => Lt
-  | Npos n', 0 => Gt
-  | Npos n', Npos m' => (n' ?= m')%positive
+  | 0, pos m' => Lt
+  | pos n', 0 => Gt
+  | pos n', pos m' => (n' ?= m')%positive
   end.
 
 Infix "?=" := compare (at level 70, no associativity) : N_scope.
@@ -119,7 +123,7 @@ Infix "?=" := compare (at level 70, no associativity) : N_scope.
 Fixpoint eqb n m :=
   match n, m with
     | 0, 0 => true
-    | Npos p, Npos q => Pos.eqb p q
+    | pos p, pos q => Pos.eqb p q
     | _, _ => false
   end.
 
@@ -151,8 +155,8 @@ Definition div2 n :=
   match n with
   | 0 => 0
   | 1 => 0
-  | Npos (p~0) => Npos p
-  | Npos (p~1) => Npos p
+  | pos (p~0) => pos p
+  | pos (p~1) => pos p
   end.
 
 (** Parity *)
@@ -160,7 +164,7 @@ Definition div2 n :=
 Definition even n :=
   match n with
     | 0 => true
-    | Npos (xO _) => true
+    | pos (xO _) => true
     | _ => false
   end.
 
@@ -172,7 +176,7 @@ Definition pow n p :=
   match p, n with
     | 0, _ => 1
     | _, 0 => 0
-    | Npos p, Npos q => Npos (q^p)
+    | pos p, pos q => pos (q^p)
   end.
 
 Infix "^" := pow : N_scope.
@@ -182,7 +186,7 @@ Infix "^" := pow : N_scope.
 Definition square n :=
   match n with
     | 0 => 0
-    | Npos p => Npos (Pos.square p)
+    | pos p => pos (Pos.square p)
   end.
 
 (** Base-2 logarithm *)
@@ -191,8 +195,8 @@ Definition log2 n :=
  match n with
    | 0 => 0
    | 1 => 0
-   | Npos (p~0) => Npos (Pos.size p)
-   | Npos (p~1) => Npos (Pos.size p)
+   | pos (p~0) => pos (Pos.size p)
+   | pos (p~1) => pos (Pos.size p)
  end.
 
 (** How many digits in a number ?
@@ -202,13 +206,13 @@ Definition log2 n :=
 Definition size n :=
  match n with
   | 0 => 0
-  | Npos p => Npos (Pos.size p)
+  | pos p => pos (Pos.size p)
  end.
 
 Definition size_nat n :=
  match n with
   | 0 => O
-  | Npos p => Pos.size_nat p
+  | pos p => Pos.size_nat p
  end.
 
 (** Euclidean division *)
@@ -233,7 +237,7 @@ Definition div_eucl (a b:N) : N * N :=
   match a, b with
    | 0,  _ => (0, 0)
    | _, 0  => (0, a)
-   | Npos na, _ => pos_div_eucl na b
+   | pos na, _ => pos_div_eucl na b
   end.
 
 Definition div a b := fst (div_eucl a b).
@@ -248,7 +252,7 @@ Definition gcd a b :=
  match a, b with
   | 0, _ => b
   | _, 0 => a
-  | Npos p, Npos q => Npos (Pos.gcd p q)
+  | pos p, pos q => pos (Pos.gcd p q)
  end.
 
 (** Generalized Gcd, also computing rests of [a] and [b] after
@@ -258,9 +262,9 @@ Definition ggcd a b :=
  match a, b with
   | 0, _ => (b,(0,1))
   | _, 0 => (a,(1,0))
-  | Npos p, Npos q =>
+  | pos p, pos q =>
      let '(g,(aa,bb)) := Pos.ggcd p q in
-     (Npos g, (Npos aa, Npos bb))
+     (pos g, (pos aa, pos bb))
  end.
 
 (** Square root *)
@@ -268,17 +272,17 @@ Definition ggcd a b :=
 Definition sqrtrem n :=
  match n with
   | 0 => (0, 0)
-  | Npos p =>
+  | pos p =>
     match Pos.sqrtrem p with
-     | (s, IsPos r) => (Npos s, Npos r)
-     | (s, _) => (Npos s, 0)
+     | (s, IsPos r) => (pos s, pos r)
+     | (s, _) => (pos s, 0)
     end
  end.
 
 Definition sqrt n :=
  match n with
   | 0 => 0
-  | Npos p => Npos (Pos.sqrt p)
+  | pos p => pos (Pos.sqrt p)
  end.
 
 (** Operation over bits of a [N] number. *)
@@ -289,7 +293,7 @@ Definition lor n m :=
  match n, m with
    | 0, _ => m
    | _, 0 => n
-   | Npos p, Npos q => Npos (Pos.lor p q)
+   | pos p, pos q => pos (Pos.lor p q)
  end.
 
 (** Logical [and] *)
@@ -298,7 +302,7 @@ Definition land n m :=
  match n, m with
   | 0, _ => 0
   | _, 0 => 0
-  | Npos p, Npos q => Pos.land p q
+  | pos p, pos q => Pos.land p q
  end.
 
 (** Logical [diff] *)
@@ -307,7 +311,7 @@ Fixpoint ldiff n m :=
  match n, m with
   | 0, _ => 0
   | _, 0 => n
-  | Npos p, Npos q => Pos.ldiff p q
+  | pos p, pos q => Pos.ldiff p q
  end.
 
 (** [xor] *)
@@ -316,7 +320,7 @@ Definition lxor n m :=
   match n, m with
     | 0, _ => m
     | _, 0 => n
-    | Npos p, Npos q => Pos.lxor p q
+    | pos p, pos q => Pos.lxor p q
   end.
 
 (** Shifts *)
@@ -327,13 +331,13 @@ Definition shiftr_nat (a:N)(n:nat) := nat_iter n div2 a.
 Definition shiftl a n :=
   match a with
     | 0 => 0
-    | Npos a => Npos (Pos.shiftl a n)
+    | pos a => pos (Pos.shiftl a n)
   end.
 
 Definition shiftr a n :=
   match n with
     | 0 => a
-    | Npos p => Pos.iter p div2 a
+    | pos p => Pos.iter p div2 a
   end.
 
 (** Checking whether a particular bit is set or not *)
@@ -341,7 +345,7 @@ Definition shiftr a n :=
 Definition testbit_nat (a:N) :=
   match a with
     | 0 => fun _ => false
-    | Npos p => Pos.testbit_nat p
+    | pos p => Pos.testbit_nat p
   end.
 
 (** Same, but with index in N *)
@@ -349,7 +353,7 @@ Definition testbit_nat (a:N) :=
 Definition testbit a n :=
   match a with
     | 0 => false
-    | Npos p => Pos.testbit p n
+    | pos p => Pos.testbit p n
   end.
 
 (** Translation from [N] to [nat] and back. *)
@@ -357,13 +361,13 @@ Definition testbit a n :=
 Definition to_nat (a:N) :=
   match a with
     | 0 => O
-    | Npos p => Pos.to_nat p
+    | pos p => Pos.to_nat p
   end.
 
 Definition of_nat (n:nat) :=
   match n with
     | O => 0
-    | S n' => Npos (Pos.of_succ_nat n')
+    | S n' => pos (Pos.of_succ_nat n')
   end.
 
 (** Iteration of a function *)
@@ -371,7 +375,7 @@ Definition of_nat (n:nat) :=
 Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
   match n with
     | 0 => x
-    | Npos p => Pos.iter p f x
+    | pos p => Pos.iter p f x
   end.
 
 End N.
\ No newline at end of file
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index f2ee29cc0..ee0b2ebc4 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -15,315 +15,238 @@ Require Import Pnat.
 Require Import Nnat.
 Require Import Ndigits.
 
-(** A boolean equality over [N] *)
+Local Open Scope N_scope.
 
-Notation Peqb := Peqb (only parsing). (* Now in [BinPos] *)
-Notation Neqb := Neqb (only parsing). (* Now in [BinNat] *)
+(** Obsolete results about boolean comparisons over [N],
+    kept for compatibility with IntMap and SMC. *)
 
-Notation Peqb_correct := Peqb_refl (only parsing).
+Notation Peqb := Pos.eqb (compat "8.3").
+Notation Neqb := N.eqb (compat "8.3").
+Notation Peqb_correct := Pos.eqb_refl (compat "8.3").
+Notation Neqb_correct := N.eqb_refl (compat "8.3").
+Notation Neqb_comm := N.eqb_sym (compat "8.3").
 
-Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'.
-Proof.
-  intros. now apply (Peqb_eq p p').
-Qed.
+Lemma Peqb_complete p p' : Pos.eqb p p' = true -> p = p'.
+Proof. now apply Pos.eqb_eq. Qed.
 
-Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pos.compare p p' = Eq.
-Proof.
-  intros. now rewrite Pos.compare_eq_iff, <- Peqb_eq.
-Qed.
-
-Lemma Pcompare_Peqb : forall p p', Pos.compare p p' = Eq -> Peqb p p' = true.
-Proof.
-  intros; now rewrite Peqb_eq, <- Pos.compare_eq_iff.
-Qed.
+Lemma Peqb_Pcompare p p' : Pos.eqb p p' = true -> Pos.compare p p' = Eq.
+Proof. now rewrite Pos.compare_eq_iff, <- Pos.eqb_eq. Qed.
 
-Lemma Neqb_correct : forall n, Neqb n n = true.
-Proof.
-  intros; now rewrite Neqb_eq.
-Qed.
+Lemma Pcompare_Peqb p p' : Pos.compare p p' = Eq -> Pos.eqb p p' = true.
+Proof. now rewrite Pos.eqb_eq, <- Pos.compare_eq_iff. Qed.
 
-Lemma Neqb_Ncompare : forall n n', Neqb n n' = true -> Ncompare n n' = Eq.
-Proof.
-  intros; now rewrite Ncompare_eq_correct, <- Neqb_eq.
-Qed.
+Lemma Neqb_Ncompare n n' : N.eqb n n' = true -> N.compare n n' = Eq.
+Proof. now rewrite N.compare_eq_iff, <- N.eqb_eq. Qed.
 
-Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true.
-Proof.
-  intros; now rewrite Neqb_eq, <- Ncompare_eq_correct.
-Qed.
+Lemma Ncompare_Neqb n n' : N.compare n n' = Eq -> N.eqb n n' = true.
+Proof. now rewrite N.eqb_eq, <- N.compare_eq_iff. Qed.
 
-Lemma Neqb_complete : forall a a', Neqb a a' = true -> a = a'.
-Proof.
-  intros; now rewrite <- Neqb_eq.
-Qed.
+Lemma Neqb_complete n n' : N.eqb n n' = true -> n = n'.
+Proof. now apply N.eqb_eq. Qed.
 
-Lemma Neqb_comm : forall a a', Neqb a a' = Neqb a' a.
+Lemma Nxor_eq_true n n' : N.lxor n n' = 0 -> N.eqb n n' = true.
 Proof.
-  intros; apply eq_true_iff_eq. rewrite 2 Neqb_eq; auto with *.
+  intro H. apply N.lxor_eq in H. subst. apply N.eqb_refl.
 Qed.
 
-Lemma Nxor_eq_true :
- forall a a', Nxor a a' = N0 -> Neqb a a' = true.
-Proof.
-  intros. rewrite (Nxor_eq a a' H). apply Neqb_correct.
-Qed.
+Ltac eqb2eq := rewrite <- ?not_true_iff_false in *; rewrite ?N.eqb_eq in *.
 
-Lemma Nxor_eq_false :
- forall a a' p, Nxor a a' = Npos p -> Neqb a a' = false.
+Lemma Nxor_eq_false n n' p :
+  N.lxor n n' = N.pos p -> N.eqb n n' = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a a')). intro H0.
-  rewrite (Neqb_complete a a' H0) in H.
-  rewrite (Nxor_nilpotent a') in H. discriminate H.
-  trivial.
+  intros. eqb2eq. intro. subst. now rewrite N.lxor_nilpotent in *.
 Qed.
 
-Lemma Nodd_not_double :
- forall a,
-   Nodd a -> forall a0, Neqb (Ndouble a0) a = false.
+Lemma Nodd_not_double a :
+  Nodd a -> forall a0, N.eqb (N.double a0) a = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H.
-  unfold Nodd in H.
-  rewrite (Ndouble_bit0 a0) in H. discriminate H.
-  trivial.
+  intros. eqb2eq. intros <-.
+  unfold Nodd in *. now rewrite Ndouble_bit0 in *.
 Qed.
 
-Lemma Nnot_div2_not_double :
- forall a a0,
-   Neqb (Ndiv2 a) a0 = false -> Neqb a (Ndouble a0) = false.
+Lemma Nnot_div2_not_double a a0 :
+  N.eqb (N.div2 a) a0 = false -> N.eqb a (N.double a0) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H. rewrite (Ndouble_div2 a0) in H.
-  rewrite (Neqb_correct a0) in H. discriminate H.
-  intro. rewrite Neqb_comm. assumption.
+  intros H. eqb2eq. contradict H. subst. apply N.div2_double.
 Qed.
 
-Lemma Neven_not_double_plus_one :
- forall a,
-   Neven a -> forall a0, Neqb (Ndouble_plus_one a0) a = false.
+Lemma Neven_not_double_plus_one a :
+  Neven a -> forall a0, N.eqb (N.succ_double a0) a = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndouble_plus_one a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H.
-  unfold Neven in H.
-  rewrite (Ndouble_plus_one_bit0 a0) in H.
-  discriminate H.
-  trivial.
+  intros. eqb2eq. intros <-.
+  unfold Neven in *. now rewrite Ndouble_plus_one_bit0 in *.
 Qed.
 
-Lemma Nnot_div2_not_double_plus_one :
- forall a a0,
-   Neqb (Ndiv2 a) a0 = false -> Neqb (Ndouble_plus_one a0) a = false.
+Lemma Nnot_div2_not_double_plus_one a a0 :
+  N.eqb (N.div2 a) a0 = false -> N.eqb (N.succ_double a0) a = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a (Ndouble_plus_one a0))). intro H0.
-  rewrite (Neqb_complete _ _ H0) in H. rewrite (Ndouble_plus_one_div2 a0) in H.
-  rewrite (Neqb_correct a0) in H. discriminate H.
-  intro H0. rewrite Neqb_comm. assumption.
+  intros H. eqb2eq. contradict H. subst. apply N.div2_succ_double.
 Qed.
 
-Lemma Nbit0_neq :
- forall a a',
-   Nbit0 a = false -> Nbit0 a' = true -> Neqb a a' = false.
+Lemma Nbit0_neq a a' :
+  N.odd a = false -> N.odd a' = true -> N.eqb a a' = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a a')). intro H1.
-  rewrite (Neqb_complete _ _ H1) in H.
-  rewrite H in H0. discriminate H0.
-  trivial.
+  intros. eqb2eq. now intros <-.
 Qed.
 
-Lemma Ndiv2_eq :
- forall a a', Neqb a a' = true -> Neqb (Ndiv2 a) (Ndiv2 a') = true.
+Lemma Ndiv2_eq a a' :
+  N.eqb a a' = true -> N.eqb (N.div2 a) (N.div2 a') = true.
 Proof.
-  intros. cut (a = a'). intros. rewrite H0. apply Neqb_correct.
-  apply Neqb_complete. exact H.
+  intros. eqb2eq. now subst.
 Qed.
 
-Lemma Ndiv2_neq :
- forall a a',
-   Neqb (Ndiv2 a) (Ndiv2 a') = false -> Neqb a a' = false.
+Lemma Ndiv2_neq a a' :
+  N.eqb (N.div2 a) (N.div2 a') = false -> N.eqb a a' = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a a')). intro H0.
-  rewrite (Neqb_complete _ _ H0) in H.
-  rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H.
-  trivial.
+  intros H. eqb2eq. contradict H. now subst.
 Qed.
 
-Lemma Ndiv2_bit_eq :
- forall a a',
-   Nbit0 a = Nbit0 a' -> Ndiv2 a = Ndiv2 a' -> a = a'.
+Lemma Ndiv2_bit_eq a a' :
+  N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'.
 Proof.
-  intros. apply Nbit_faithful. unfold eqf in |- *. destruct n.
-  rewrite Nbit0_correct. rewrite Nbit0_correct. assumption.
-  rewrite <- Ndiv2_correct. rewrite <- Ndiv2_correct.
-  rewrite H0. reflexivity.
+  intros H H'; now rewrite (N.div2_odd a), (N.div2_odd a'), H, H'.
 Qed.
 
-Lemma Ndiv2_bit_neq :
- forall a a',
-   Neqb a a' = false ->
-   Nbit0 a = Nbit0 a' -> Neqb (Ndiv2 a) (Ndiv2 a') = false.
+Lemma Ndiv2_bit_neq a a' :
+  N.eqb a a' = false ->
+   N.odd a = N.odd a' -> N.eqb (N.div2 a) (N.div2 a') = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb (Ndiv2 a) (Ndiv2 a'))). intro H1.
-  rewrite (Ndiv2_bit_eq _ _ H0 (Neqb_complete _ _ H1)) in H.
-  rewrite (Neqb_correct a') in H. discriminate H.
-  trivial.
+  intros H H'. eqb2eq. contradict H. now apply Ndiv2_bit_eq.
 Qed.
 
-Lemma Nneq_elim :
- forall a a',
-   Neqb a a' = false ->
-   Nbit0 a = negb (Nbit0 a') \/
-   Neqb (Ndiv2 a) (Ndiv2 a') = false.
+Lemma Nneq_elim a a' :
+   N.eqb a a' = false ->
+   N.odd a = negb (N.odd a') \/
+   N.eqb (N.div2 a) (N.div2 a') = false.
 Proof.
-  intros. cut (Nbit0 a = Nbit0 a' \/ Nbit0 a = negb (Nbit0 a')).
+  intros. cut (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')).
   intros. elim H0. intro. right. apply Ndiv2_bit_neq. assumption.
   assumption.
   intro. left. assumption.
-  case (Nbit0 a); case (Nbit0 a'); auto.
+  case (N.odd a), (N.odd a'); auto.
 Qed.
 
-Lemma Ndouble_or_double_plus_un :
- forall a,
-   {a0 : N | a = Ndouble a0} + {a1 : N | a = Ndouble_plus_one a1}.
+Lemma Ndouble_or_double_plus_un a :
+   {a0 : N | a = N.double a0} + {a1 : N | a = N.succ_double a1}.
 Proof.
-  intro. elim (sumbool_of_bool (Nbit0 a)). intro H. right. split with (Ndiv2 a).
-  rewrite (Ndiv2_double_plus_one a H). reflexivity.
-  intro H. left. split with (Ndiv2 a). rewrite (Ndiv2_double a H). reflexivity.
+  elim (sumbool_of_bool (N.odd a)); intros H; [right|left];
+    exists (N.div2 a); symmetry;
+    apply Ndiv2_double_plus_one || apply Ndiv2_double; auto.
 Qed.
 
-(** A boolean order on [N] *)
+(** An inefficient boolean order on [N]. Please use [N.leb] instead now. *)
 
-Definition Nleb (a b:N) := leb (nat_of_N a) (nat_of_N b).
+Definition Nleb (a b:N) := leb (N.to_nat a) (N.to_nat b).
 
-Lemma Nleb_Nle : forall a b, Nleb a b = true <-> Nle a b.
+Lemma Nleb_alt a b : Nleb a b = N.leb a b.
 Proof.
- intros; unfold Nle; rewrite nat_of_Ncompare.
- unfold Nleb; apply leb_compare.
+ unfold Nleb.
+ now rewrite eq_iff_eq_true, N.leb_le, leb_compare, <- N2Nat.inj_compare.
 Qed.
 
-Lemma Nleb_refl : forall a, Nleb a a = true.
-Proof.
-  intro. unfold Nleb in |- *. apply leb_correct. apply le_n.
-Qed.
+Lemma Nleb_Nle a b : Nleb a b = true <-> a <= b.
+Proof. now rewrite Nleb_alt, N.leb_le. Qed.
 
-Lemma Nleb_antisym :
- forall a b, Nleb a b = true -> Nleb b a = true -> a = b.
-Proof.
-  unfold Nleb in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b).
-  rewrite (le_antisym _ _ (leb_complete _ _ H) (leb_complete _ _ H0)). reflexivity.
-Qed.
+Lemma Nleb_refl a : Nleb a a = true.
+Proof. rewrite Nleb_Nle; apply N.le_refl. Qed.
 
-Lemma Nleb_trans :
- forall a b c, Nleb a b = true -> Nleb b c = true -> Nleb a c = true.
-Proof.
-  unfold Nleb in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b).
-  apply leb_complete. assumption.
-  apply leb_complete. assumption.
-Qed.
+Lemma Nleb_antisym a b : Nleb a b = true -> Nleb b a = true -> a = b.
+Proof. rewrite !Nleb_Nle. apply N.le_antisymm. Qed.
+
+Lemma Nleb_trans a b c : Nleb a b = true -> Nleb b c = true -> Nleb a c = true.
+Proof. rewrite !Nleb_Nle. apply N.le_trans. Qed.
 
-Lemma Nleb_ltb_trans :
- forall a b c,
-   Nleb a b = true -> Nleb c b = false -> Nleb c a = false.
+Lemma Nleb_ltb_trans a b c :
+  Nleb a b = true -> Nleb c b = false -> Nleb c a = false.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b).
+  unfold Nleb. intros. apply leb_correct_conv.
+  apply le_lt_trans with (m := N.to_nat b).
   apply leb_complete. assumption.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nltb_leb_trans :
- forall a b c,
-   Nleb b a = false -> Nleb b c = true -> Nleb c a = false.
+Lemma Nltb_leb_trans a b c :
+  Nleb b a = false -> Nleb b c = true -> Nleb c a = false.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b).
+  unfold Nleb. intros. apply leb_correct_conv.
+  apply lt_le_trans with (m := N.to_nat b).
   apply leb_complete_conv. assumption.
   apply leb_complete. assumption.
 Qed.
 
-Lemma Nltb_trans :
- forall a b c,
-   Nleb b a = false -> Nleb c b = false -> Nleb c a = false.
+Lemma Nltb_trans a b c :
+  Nleb b a = false -> Nleb c b = false -> Nleb c a = false.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b).
+  unfold Nleb. intros. apply leb_correct_conv.
+  apply lt_trans with (m := N.to_nat b).
   apply leb_complete_conv. assumption.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nltb_leb_weak : forall a b:N, Nleb b a = false -> Nleb a b = true.
+Lemma Nltb_leb_weak a b : Nleb b a = false -> Nleb a b = true.
 Proof.
-  unfold Nleb in |- *. intros. apply leb_correct. apply lt_le_weak.
+  unfold Nleb. intros. apply leb_correct. apply lt_le_weak.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nleb_double_mono :
- forall a b,
-   Nleb a b = true -> Nleb (Ndouble a) (Ndouble b) = true.
+Lemma Nleb_double_mono a b :
+  Nleb a b = true -> Nleb (N.double a) (N.double b) = true.
 Proof.
-  unfold Nleb in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct.
-  simpl in |- *. apply plus_le_compat. apply leb_complete. assumption.
-  apply plus_le_compat. apply leb_complete. assumption.
-  apply le_n.
+  unfold Nleb. intros. rewrite !N2Nat.inj_double. apply leb_correct.
+  apply mult_le_compat_l. now apply leb_complete.
 Qed.
 
-Lemma Nleb_double_plus_one_mono :
- forall a b,
-   Nleb a b = true ->
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true.
+Lemma Nleb_double_plus_one_mono a b :
+  Nleb a b = true ->
+   Nleb (N.succ_double a) (N.succ_double b) = true.
 Proof.
-  unfold Nleb in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
-  apply leb_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply leb_complete.
-  assumption.
-  apply plus_le_compat. apply leb_complete. assumption.
-  apply le_n.
+  unfold Nleb. intros. rewrite !N2Nat.inj_succ_double. apply leb_correct.
+  apply le_n_S, mult_le_compat_l. now apply leb_complete.
 Qed.
 
-Lemma Nleb_double_mono_conv :
- forall a b,
-   Nleb (Ndouble a) (Ndouble b) = true -> Nleb a b = true.
+Lemma Nleb_double_mono_conv a b :
+  Nleb (N.double a) (N.double b) = true -> Nleb a b = true.
 Proof.
-  unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro.
-  apply leb_correct. apply (mult_S_le_reg_l 1). apply leb_complete. assumption.
+  unfold Nleb. rewrite !N2Nat.inj_double. intro. apply leb_correct.
+  apply (mult_S_le_reg_l 1). now apply leb_complete.
 Qed.
 
-Lemma Nleb_double_plus_one_mono_conv :
- forall a b,
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true ->
+Lemma Nleb_double_plus_one_mono_conv a b :
+  Nleb (N.succ_double a) (N.succ_double b) = true ->
    Nleb a b = true.
 Proof.
-  unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
-  intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply leb_complete.
-  assumption.
+  unfold Nleb. rewrite !N2Nat.inj_succ_double. intro. apply leb_correct.
+  apply (mult_S_le_reg_l 1). apply le_S_n. now apply leb_complete.
 Qed.
 
-Lemma Nltb_double_mono :
- forall a b,
-   Nleb a b = false -> Nleb (Ndouble a) (Ndouble b) = false.
+Lemma Nltb_double_mono a b :
+   Nleb a b = false -> Nleb (N.double a) (N.double b) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nleb (Ndouble a) (Ndouble b))). intro H0.
+  intros. elim (sumbool_of_bool (Nleb (N.double a) (N.double b))). intro H0.
   rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nltb_double_plus_one_mono :
- forall a b,
-   Nleb a b = false ->
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false.
+Lemma Nltb_double_plus_one_mono a b :
+  Nleb a b = false ->
+   Nleb (N.succ_double a) (N.succ_double b) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nleb (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0.
+  intros. elim (sumbool_of_bool (Nleb (N.succ_double a) (N.succ_double b))).
+  intro H0.
   rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nltb_double_mono_conv :
- forall a b,
-   Nleb (Ndouble a) (Ndouble b) = false -> Nleb a b = false.
+Lemma Nltb_double_mono_conv a b :
+  Nleb (N.double a) (N.double b) = false -> Nleb a b = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nleb a b)). intro H0. rewrite (Nleb_double_mono _ _ H0) in H.
-  discriminate H.
+  intros. elim (sumbool_of_bool (Nleb a b)). intro H0.
+  rewrite (Nleb_double_mono _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nltb_double_plus_one_mono_conv :
- forall a b,
-   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false ->
+Lemma Nltb_double_plus_one_mono_conv a b :
+  Nleb (N.succ_double a) (N.succ_double b) = false ->
    Nleb a b = false.
 Proof.
   intros. elim (sumbool_of_bool (Nleb a b)). intro H0.
@@ -331,110 +254,52 @@ Proof.
   trivial.
 Qed.
 
-(* Nleb and Ncompare *)
+(* Nleb and N.compare *)
 
-(* NB: No need to prove that Nleb a b = true <-> Ncompare a b <> Gt,
+(* NB: No need to prove that Nleb a b = true <-> N.compare a b <> Gt,
    this statement is in fact Nleb_Nle! *)
 
-Lemma Nltb_Ncompare : forall a b,
- Nleb a b = false <-> Ncompare a b = Gt.
+Lemma Nltb_Ncompare a b : Nleb a b = false <-> N.compare a b = Gt.
 Proof.
- intros.
- assert (IFF : forall x:bool, x = false <-> ~ x = true)
-   by (destruct x; intuition).
- rewrite IFF, Nleb_Nle; unfold Nle.
- destruct (Ncompare a b); split; intro H; auto;
-  elim H; discriminate.
+  now rewrite N.compare_nle_iff, <- Nleb_Nle, not_true_iff_false.
 Qed.
 
-Lemma Ncompare_Gt_Nltb : forall a b,
- Ncompare a b = Gt -> Nleb a b = false.
-Proof.
- intros; apply <- Nltb_Ncompare; auto.
-Qed.
+Lemma Ncompare_Gt_Nltb a b : N.compare a b = Gt -> Nleb a b = false.
+Proof. apply <- Nltb_Ncompare; auto. Qed.
 
-Lemma Ncompare_Lt_Nltb : forall a b,
- Ncompare a b = Lt -> Nleb b a = false.
+Lemma Ncompare_Lt_Nltb a b : N.compare a b = Lt -> Nleb b a = false.
 Proof.
- intros a b H.
- rewrite Nltb_Ncompare, <- Ncompare_antisym, H; auto.
+ intros H. rewrite Nltb_Ncompare, N.compare_antisym, H; auto.
 Qed.
 
-(* An alternate [min] function over [N] *)
+(* Old results about [N.min] *)
 
-Definition Nmin' (a b:N) := if Nleb a b then a else b.
+Notation Nmin_choice := N.min_dec (compat "8.3").
 
-Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b.
-Proof.
- unfold Nmin, Nmin', Nleb; intros.
- rewrite nat_of_Ncompare.
- generalize (leb_compare (nat_of_N a) (nat_of_N b));
- destruct (nat_compare (nat_of_N a) (nat_of_N b));
- destruct (leb (nat_of_N a) (nat_of_N b)); intuition.
- lapply H1; intros; discriminate.
- lapply H1; intros; discriminate.
-Qed.
+Lemma Nmin_le_1 a b : Nleb (N.min a b) a = true.
+Proof. rewrite Nleb_Nle. apply N.le_min_l. Qed.
 
-Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}.
-Proof.
-  unfold Nmin in *; intros; destruct (Ncompare a b); auto.
-Qed.
+Lemma Nmin_le_2 a b : Nleb (N.min a b) b = true.
+Proof. rewrite Nleb_Nle. apply N.le_min_r. Qed.
 
-Lemma Nmin_le_1 : forall a b, Nleb (Nmin a b) a = true.
-Proof.
-  intros; rewrite Nmin_Nmin'.
-  unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H.
-  apply Nleb_refl.
-  intro H. rewrite H. apply Nltb_leb_weak. assumption.
-Qed.
+Lemma Nmin_le_3 a b c : Nleb a (N.min b c) = true -> Nleb a b = true.
+Proof. rewrite !Nleb_Nle. apply N.min_glb_l. Qed.
 
-Lemma Nmin_le_2 : forall a b, Nleb (Nmin a b) b = true.
-Proof.
-  intros; rewrite Nmin_Nmin'.
-  unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. assumption.
-  intro H. rewrite H. apply Nleb_refl.
-Qed.
+Lemma Nmin_le_4 a b c : Nleb a (N.min b c) = true -> Nleb a c = true.
+Proof. rewrite !Nleb_Nle. apply N.min_glb_r. Qed.
 
-Lemma Nmin_le_3 :
- forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true.
-Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  assumption.
-  intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption.
-Qed.
+Lemma Nmin_le_5 a b c :
+   Nleb a b = true -> Nleb a c = true -> Nleb a (N.min b c) = true.
+Proof. rewrite !Nleb_Nle. apply N.min_glb. Qed.
 
-Lemma Nmin_le_4 :
- forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true.
+Lemma Nmin_lt_3 a b c : Nleb (N.min b c) a = false -> Nleb b a = false.
 Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  apply Nleb_trans with (b := b); assumption.
-  intro H0. rewrite H0 in H. assumption.
-Qed.
-
-Lemma Nmin_le_5 :
- forall a b c,
-   Nleb a b = true -> Nleb a c = true -> Nleb a (Nmin b c) = true.
-Proof.
-  intros. elim (Nmin_choice b c). intro H1. rewrite H1. assumption.
-  intro H1. rewrite H1. assumption.
-Qed.
-
-Lemma Nmin_lt_3 :
- forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false.
-Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  assumption.
-  intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption.
+  rewrite <- !not_true_iff_false, !Nleb_Nle.
+  rewrite N.min_le_iff; auto.
 Qed.
 
-Lemma Nmin_lt_4 :
- forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false.
+Lemma Nmin_lt_4 a b c : Nleb (N.min b c) a = false -> Nleb c a = false.
 Proof.
-  intros; rewrite Nmin_Nmin' in *.
-  unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
-  apply Nltb_leb_trans with (b := b); assumption.
-  intro H0. rewrite H0 in H. assumption.
+  rewrite <- !not_true_iff_false, !Nleb_Nle.
+  rewrite N.min_le_iff; auto.
 Qed.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 06f47d719..77364e5ea 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -31,25 +31,25 @@ Notation Nxor_nilpotent := N.lxor_nilpotent (compat "8.3").
     either with index in [N] or in [nat]. *)
 
 Lemma Ptestbit_Pbit :
- forall p n, Pos.testbit p (N.of_nat n) = Pbit p n.
+ forall p n, Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n.
 Proof.
  induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial;
-  rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite N_of_pred.
+  rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite Nat2N.inj_pred.
 Qed.
 
-Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = Nbit a n.
+Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = N.testbit_nat a n.
 Proof.
  destruct a. trivial. apply Ptestbit_Pbit.
 Qed.
 
 Lemma Pbit_Ptestbit :
- forall p n, Pbit p (N.to_nat n) = Pos.testbit p n.
+ forall p n, Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n.
 Proof.
  intros; now rewrite <- Ptestbit_Pbit, N2Nat.id.
 Qed.
 
 Lemma Nbit_Ntestbit :
- forall a n, Nbit a (N.to_nat n) = N.testbit a n.
+ forall a n, N.testbit_nat a (N.to_nat n) = N.testbit a n.
 Proof.
  destruct a. trivial. apply Pbit_Ptestbit.
 Qed.
@@ -73,7 +73,7 @@ Lemma Nshiftr_nat_equiv :
 Proof.
  intros a [|n]; simpl. unfold N.shiftr_nat.
  trivial.
- symmetry. apply iter_nat_of_P.
+ symmetry. apply Pos2Nat.inj_iter.
 Qed.
 
 Lemma Nshiftr_equiv_nat :
@@ -99,7 +99,7 @@ Qed.
 (** Correctness proofs for shifts, nat version *)
 
 Lemma Nshiftr_nat_spec : forall a n m,
-  Nbit (N.shiftr_nat a n) m = Nbit a (m+n).
+  N.testbit_nat (N.shiftr_nat a n) m = N.testbit_nat a (m+n).
 Proof.
  induction n; intros m.
  now rewrite <- plus_n_O.
@@ -108,7 +108,7 @@ Proof.
 Qed.
 
 Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
-  Nbit (N.shiftl_nat a n) m = Nbit a (m-n).
+  N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n).
 Proof.
  induction n; intros m H.
  now rewrite <- minus_n_O.
@@ -118,7 +118,7 @@ Proof.
 Qed.
 
 Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
- Nbit (N.shiftl_nat a n) m = false.
+ N.testbit_nat (N.shiftl_nat a n) m = false.
 Proof.
  induction n; intros m H. inversion H.
  rewrite Nshiftl_nat_S.
@@ -151,52 +151,52 @@ Proof.
  rewrite 2 Pshiftl_nat_S. now f_equal.
 Qed.
 
-(** Semantics of bitwise operations with respect to [Nbit] *)
+(** Semantics of bitwise operations with respect to [N.testbit_nat] *)
 
 Lemma Pxor_semantics p p' n :
- Nbit (Pos.lxor p p') n = xorb (Pbit p n) (Pbit p' n).
+ N.testbit_nat (Pos.lxor p p') n = xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n).
 Proof.
  rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_lxor_spec.
 Qed.
 
 Lemma Nxor_semantics a a' n :
- Nbit (N.lxor a a') n = xorb (Nbit a n) (Nbit a' n).
+ N.testbit_nat (N.lxor a a') n = xorb (N.testbit_nat a n) (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.lxor_spec.
 Qed.
 
 Lemma Por_semantics p p' n :
- Pbit (Pos.lor p p') n = (Pbit p n) || (Pbit p' n).
+ Pos.testbit_nat (Pos.lor p p') n = (Pos.testbit_nat p n) || (Pos.testbit_nat p' n).
 Proof.
  rewrite <- !Ptestbit_Pbit. apply N.pos_lor_spec.
 Qed.
 
 Lemma Nor_semantics a a' n :
- Nbit (N.lor a a') n = (Nbit a n) || (Nbit a' n).
+ N.testbit_nat (N.lor a a') n = (N.testbit_nat a n) || (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.lor_spec.
 Qed.
 
 Lemma Pand_semantics p p' n :
- Nbit (Pos.land p p') n = (Pbit p n) && (Pbit p' n).
+ N.testbit_nat (Pos.land p p') n = (Pos.testbit_nat p n) && (Pos.testbit_nat p' n).
 Proof.
  rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_land_spec.
 Qed.
 
 Lemma Nand_semantics a a' n :
- Nbit (N.land a a') n = (Nbit a n) && (Nbit a' n).
+ N.testbit_nat (N.land a a') n = (N.testbit_nat a n) && (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.land_spec.
 Qed.
 
 Lemma Pdiff_semantics p p' n :
- Nbit (Pos.ldiff p p') n = (Pbit p n) && negb (Pbit p' n).
+ N.testbit_nat (Pos.ldiff p p') n = (Pos.testbit_nat p n) && negb (Pos.testbit_nat p' n).
 Proof.
  rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_ldiff_spec.
 Qed.
 
 Lemma Ndiff_semantics a a' n :
- Nbit (N.ldiff a a') n = (Nbit a n) && negb (Nbit a' n).
+ N.testbit_nat (N.ldiff a a') n = (N.testbit_nat a n) && negb (N.testbit_nat a' n).
 Proof.
  rewrite <- !Ntestbit_Nbit. apply N.ldiff_spec.
 Qed.
@@ -213,13 +213,13 @@ Local Infix "==" := eqf (at level 70, no associativity).
 
 Local Notation Step H := (fun n => H (S n)).
 
-Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)).
+Lemma Pbit_faithful_0 : forall p, ~(Pos.testbit_nat p == (fun _ => false)).
 Proof.
  induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O).
   apply (IHp (Step H)).
 Qed.
 
-Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'.
+Lemma Pbit_faithful : forall p p', Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'.
 Proof.
  induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial;
   try discriminate (H O).
@@ -229,7 +229,7 @@ Proof.
  symmetry in H. destruct (Pbit_faithful_0 _ (Step H)).
 Qed.
 
-Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'.
+Lemma Nbit_faithful : forall n n', N.testbit_nat n == N.testbit_nat n' -> n = n'.
 Proof.
  intros [|p] [|p'] H; trivial.
  symmetry in H. destruct (Pbit_faithful_0 _ H).
@@ -237,7 +237,7 @@ Proof.
  f_equal. apply Pbit_faithful, H.
 Qed.
 
-Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'.
+Lemma Nbit_faithful_iff : forall n n', N.testbit_nat n == N.testbit_nat n' <-> n = n'.
 Proof.
  split. apply Nbit_faithful. intros; now subst.
 Qed.
@@ -249,28 +249,28 @@ Local Close Scope N_scope.
 
 Notation Nbit0 := N.odd (compat "8.3").
 
-Definition Nodd (n:N) := Nbit0 n = true.
-Definition Neven (n:N) := Nbit0 n = false.
+Definition Nodd (n:N) := N.odd n = true.
+Definition Neven (n:N) := N.odd n = false.
 
-Lemma Nbit0_correct : forall n:N, Nbit n 0 = Nbit0 n.
+Lemma Nbit0_correct : forall n:N, N.testbit_nat n 0 = N.odd n.
 Proof.
   destruct n; trivial.
   destruct p; trivial.
 Qed.
 
-Lemma Ndouble_bit0 : forall n:N, Nbit0 (Ndouble n) = false.
+Lemma Ndouble_bit0 : forall n:N, N.odd (N.double n) = false.
 Proof.
   destruct n; trivial.
 Qed.
 
 Lemma Ndouble_plus_one_bit0 :
- forall n:N, Nbit0 (Ndouble_plus_one n) = true.
+ forall n:N, N.odd (N.succ_double n) = true.
 Proof.
   destruct n; trivial.
 Qed.
 
 Lemma Ndiv2_double :
- forall n:N, Neven n -> Ndouble (Ndiv2 n) = n.
+ forall n:N, Neven n -> N.double (N.div2 n) = n.
 Proof.
   destruct n. trivial. destruct p. intro H. discriminate H.
   intros. reflexivity.
@@ -278,7 +278,7 @@ Proof.
 Qed.
 
 Lemma Ndiv2_double_plus_one :
- forall n:N, Nodd n -> Ndouble_plus_one (Ndiv2 n) = n.
+ forall n:N, Nodd n -> N.succ_double (N.div2 n) = n.
 Proof.
   destruct n. intro. discriminate H.
   destruct p. intros. reflexivity.
@@ -287,31 +287,31 @@ Proof.
 Qed.
 
 Lemma Ndiv2_correct :
- forall (a:N) (n:nat), Nbit (Ndiv2 a) n = Nbit a (S n).
+ forall (a:N) (n:nat), N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n).
 Proof.
   destruct a; trivial.
   destruct p; trivial.
 Qed.
 
 Lemma Nxor_bit0 :
- forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a').
+ forall a a':N, N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a').
 Proof.
   intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O).
   rewrite Nbit0_correct, Nbit0_correct. reflexivity.
 Qed.
 
 Lemma Nxor_div2 :
- forall a a':N, Ndiv2 (Nxor a a') = Nxor (Ndiv2 a) (Ndiv2 a').
+ forall a a':N, N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a').
 Proof.
   intros. apply Nbit_faithful. unfold eqf. intro.
-  rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
+  rewrite (Nxor_semantics (N.div2 a) (N.div2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
   rewrite 2! Ndiv2_correct.
   reflexivity.
 Qed.
 
 Lemma Nneg_bit0 :
  forall a a':N,
-   Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a').
+   N.odd (N.lxor a a') = true -> N.odd a = negb (N.odd a').
 Proof.
   intros.
   rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, 
@@ -320,24 +320,24 @@ Proof.
 Qed.
 
 Lemma Nneg_bit0_1 :
- forall a a':N, Nxor a a' = Npos 1 -> Nbit0 a = negb (Nbit0 a').
+ forall a a':N, N.lxor a a' = Npos 1 -> N.odd a = negb (N.odd a').
 Proof.
   intros. apply Nneg_bit0. rewrite H. reflexivity.
 Qed.
 
 Lemma Nneg_bit0_2 :
  forall (a a':N) (p:positive),
-   Nxor a a' = Npos (xI p) -> Nbit0 a = negb (Nbit0 a').
+   N.lxor a a' = Npos (xI p) -> N.odd a = negb (N.odd a').
 Proof.
   intros. apply Nneg_bit0. rewrite H. reflexivity.
 Qed.
 
 Lemma Nsame_bit0 :
  forall (a a':N) (p:positive),
-   Nxor a a' = Npos (xO p) -> Nbit0 a = Nbit0 a'.
+   N.lxor a a' = Npos (xO p) -> N.odd a = N.odd a'.
 Proof.
-  intros. rewrite <- (xorb_false (Nbit0 a)).
-  assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity.
+  intros. rewrite <- (xorb_false (N.odd a)).
+  assert (H0: N.odd (Npos (xO p)) = false) by reflexivity.
   rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb.
     reflexivity.
 Qed.
@@ -346,77 +346,77 @@ Qed.
 
 Fixpoint Nless_aux (a a':N) (p:positive) : bool :=
   match p with
-  | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p'
-  | _ => andb (negb (Nbit0 a)) (Nbit0 a')
+  | xO p' => Nless_aux (N.div2 a) (N.div2 a') p'
+  | _ => andb (negb (N.odd a)) (N.odd a')
   end.
 
 Definition Nless (a a':N) :=
-  match Nxor a a' with
+  match N.lxor a a' with
   | N0 => false
   | Npos p => Nless_aux a a' p
   end.
 
 Lemma Nbit0_less :
  forall a a',
-   Nbit0 a = false -> Nbit0 a' = true -> Nless a a' = true.
+   N.odd a = false -> N.odd a' = true -> Nless a a' = true.
 Proof.
-  intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+  intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless.
   rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
-  assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+  assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
   simpl. rewrite H, H0. reflexivity.
-  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+  assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
 Qed.
 
 Lemma Nbit0_gt :
  forall a a',
-   Nbit0 a = true -> Nbit0 a' = false -> Nless a a' = false.
+   N.odd a = true -> N.odd a' = false -> Nless a a' = false.
 Proof.
-  intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+  intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless.
   rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
-  assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+  assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
   simpl. rewrite H, H0. reflexivity.
-  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+  assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
 Qed.
 
 Lemma Nless_not_refl : forall a, Nless a a = false.
 Proof.
-  intro. unfold Nless. rewrite (Nxor_nilpotent a). reflexivity.
+  intro. unfold Nless. rewrite (N.lxor_nilpotent a). reflexivity.
 Qed.
 
 Lemma Nless_def_1 :
- forall a a', Nless (Ndouble a) (Ndouble a') = Nless a a'.
+ forall a a', Nless (N.double a) (N.double a') = Nless a a'.
 Proof.
   destruct a; destruct a'. reflexivity.
   trivial.
   unfold Nless. simpl. destruct p; trivial.
-  unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
+  unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity.
   trivial.
 Qed.
 
 Lemma Nless_def_2 :
  forall a a',
-   Nless (Ndouble_plus_one a) (Ndouble_plus_one a') = Nless a a'.
+   Nless (N.succ_double a) (N.succ_double a') = Nless a a'.
 Proof.
   destruct a; destruct a'. reflexivity.
   trivial.
   unfold Nless. simpl. destruct p; trivial.
-  unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
+  unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity.
   trivial.
 Qed.
 
 Lemma Nless_def_3 :
- forall a a', Nless (Ndouble a) (Ndouble_plus_one a') = true.
+ forall a a', Nless (N.double a) (N.succ_double a') = true.
 Proof.
   intros. apply Nbit0_less. apply Ndouble_bit0.
   apply Ndouble_plus_one_bit0.
 Qed.
 
 Lemma Nless_def_4 :
- forall a a', Nless (Ndouble_plus_one a) (Ndouble a') = false.
+ forall a a', Nless (N.succ_double a) (N.double a') = false.
 Proof.
   intros. apply Nbit0_gt. apply Ndouble_plus_one_bit0.
   apply Ndouble_bit0.
@@ -425,7 +425,7 @@ Qed.
 Lemma Nless_z : forall a, Nless a N0 = false.
 Proof.
   induction a. reflexivity.
-  unfold Nless. rewrite (Nxor_neutral_right (Npos p)). induction p; trivial.
+  unfold Nless. rewrite (N.lxor_0_r (Npos p)). induction p; trivial.
 Qed.
 
 Lemma N0_less_1 :
@@ -445,26 +445,26 @@ Lemma Nless_trans :
  forall a a' a'',
    Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
 Proof.
-  induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0.
+  induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0.
     case_eq (Nless N0 a'') ; intros Heqn. trivial.
      rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0.
-    induction a' as [|a' _|a' _] using N_ind_double.
-      rewrite (Nless_z (Ndouble a)) in H. discriminate H.
+    induction a' as [|a' _|a' _] using N.binary_ind.
+      rewrite (Nless_z (N.double a)) in H. discriminate H.
       rewrite (Nless_def_1 a a') in H.
-       induction a'' using N_ind_double.
-         rewrite (Nless_z (Ndouble a')) in H0. discriminate H0.
+       induction a'' using N.binary_ind.
+         rewrite (Nless_z (N.double a')) in H0. discriminate H0.
          rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a'').
           exact (IHa _ _ H H0).
          apply Nless_def_3.
-      induction a'' as [|a'' _|a'' _] using N_ind_double.
-        rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+      induction a'' as [|a'' _|a'' _] using N.binary_ind.
+        rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
         rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
         apply Nless_def_3.
-    induction a' as [|a' _|a' _] using N_ind_double.
-      rewrite (Nless_z (Ndouble_plus_one a)) in H. discriminate H.
+    induction a' as [|a' _|a' _] using N.binary_ind.
+      rewrite (Nless_z (N.succ_double a)) in H. discriminate H.
       rewrite (Nless_def_4 a a') in H. discriminate H.
-      induction a'' using N_ind_double.
-        rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+      induction a'' using N.binary_ind.
+        rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
         rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
         rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H.
           rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0).
@@ -473,17 +473,17 @@ Qed.
 Lemma Nless_total :
  forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
 Proof.
-  induction a using N_rec_double; intro a'.
+  induction a using N.binary_rec; intro a'.
     case_eq (Nless N0 a') ; intros Heqb. left. left. auto.
      right. rewrite (N0_less_2 a' Heqb). reflexivity.
-    induction a' as [|a' _|a' _] using N_rec_double.
-      case_eq (Nless N0 (Ndouble a)) ; intros Heqb. left. right. auto.
+    induction a' as [|a' _|a' _] using N.binary_rec.
+      case_eq (Nless N0 (N.double a)) ; intros Heqb. left. right. auto.
        right. exact (N0_less_2 _  Heqb).
       rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
         left. assumption.
         right. reflexivity.
     left. left. apply Nless_def_3.
-    induction a' as [|a' _|a' _] using N_rec_double.
+    induction a' as [|a' _|a' _] using N.binary_rec.
       left. right. destruct a; reflexivity.
       left. right. apply Nless_def_3.
       rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->].
@@ -497,15 +497,15 @@ Notation Nsize := N.size_nat (compat "8.3").
 
 (** conversions between N and bit vectors. *)
 
-Fixpoint P2Bv (p:positive) : Bvector (Psize p) :=
- match p return Bvector (Psize p) with
+Fixpoint P2Bv (p:positive) : Bvector (Pos.size_nat p) :=
+ match p return Bvector (Pos.size_nat p) with
    | xH => Bvect_true 1%nat
-   | xO p => Bcons false (Psize p) (P2Bv p)
-   | xI p => Bcons true (Psize p) (P2Bv p)
+   | xO p => Bcons false (Pos.size_nat p) (P2Bv p)
+   | xI p => Bcons true (Pos.size_nat p) (P2Bv p)
  end.
 
-Definition N2Bv (n:N) : Bvector (Nsize n) :=
-  match n as n0 return Bvector (Nsize n0) with
+Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
+  match n as n0 return Bvector (N.size_nat n0) with
     | N0 => Bnil
     | Npos p => P2Bv p
   end.
@@ -513,8 +513,8 @@ Definition N2Bv (n:N) : Bvector (Nsize n) :=
 Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
     | Vector.nil => N0
-    | Vector.cons false n bv => Ndouble (Bv2N n bv)
-    | Vector.cons true n bv => Ndouble_plus_one (Bv2N n bv)
+    | Vector.cons false n bv => N.double (Bv2N n bv)
+    | Vector.cons true n bv => N.succ_double (Bv2N n bv)
   end.
 
 Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
@@ -528,7 +528,7 @@ Qed.
   bit vector has some zeros on its right, they will disappear during
   the return [Bv2N] translation: *)
 
-Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n.
+Lemma Bv2N_Nsize : forall n (bv:Bvector n), N.size_nat (Bv2N n bv) <= n.
 Proof.
 induction bv; intros.
 auto.
@@ -543,7 +543,7 @@ Qed.
 
 Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
   Bsign _ bv = true <->
-  Nsize (Bv2N _ bv) = (S n).
+  N.size_nat (Bv2N _ bv) = (S n).
 Proof.
 apply Vector.rectS ; intros ; simpl.
 destruct a ; compute ; split ; intros x ; now inversion x.
@@ -567,7 +567,7 @@ Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n :=
 
 (** The first [N2Bv] is then a special case of [N2Bv_gen] *)
 
-Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (Nsize a) a.
+Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (N.size_nat a) a.
 Proof.
 destruct a; simpl.
 auto.
@@ -578,7 +578,7 @@ Qed.
    [a] plus some zeros. *)
 
 Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat),
- N2Bv_gen (Nsize a + k) a = Vector.append (N2Bv a) (Bvect_false k).
+ N2Bv_gen (N.size_nat a + k) a = Vector.append (N2Bv a) (Bvect_false k).
 Proof.
 destruct a; simpl.
 destruct k; simpl; auto.
@@ -603,7 +603,7 @@ Qed.
 (** accessing some precise bits. *)
 
 Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
-  Nbit0 (Bv2N _ bv) = Blow _ bv.
+  N.odd (Bv2N _ bv) = Blow _ bv.
 Proof.
 apply Vector.caseS.
 intros.
@@ -616,7 +616,7 @@ Qed.
 Notation Bnth := (@Vector.nth_order bool).
 
 Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
-  Bnth bv H = Nbit (Bv2N _ bv) p.
+  Bnth bv H = N.testbit_nat (Bv2N _ bv) p.
 Proof.
 induction bv; intros.
 inversion H.
@@ -626,7 +626,7 @@ destruct p ; simpl.
     simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto.
 Qed.
 
-Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false.
+Lemma Nbit_Nsize : forall n p, N.size_nat n <= p -> N.testbit_nat n p = false.
 Proof.
 destruct n as [|n].
 simpl; auto.
@@ -635,7 +635,8 @@ inversion H.
 inversion H.
 Qed.
 
-Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth (N2Bv n) H.
+Lemma Nbit_Bth: forall n p (H:p < N.size_nat n),
+  N.testbit_nat n p = Bnth (N2Bv n) H.
 Proof.
 destruct n as [|n].
 inversion H.
@@ -646,7 +647,7 @@ Qed.
 (** Binary bitwise operations are the same in the two worlds. *)
 
 Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
-  Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').
+  Bv2N _ (BVxor _ bv bv') = N.lxor (Bv2N _ bv) (Bv2N _ bv').
 Proof.
 apply Vector.rect2 ; intros.
 now simpl.
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v
index 22adc5050..7097159c7 100644
--- a/theories/NArith/Ndist.v
+++ b/theories/NArith/Ndist.v
@@ -38,7 +38,7 @@ Qed.
 
 Lemma Nplength_zeros :
  forall (a:N) (n:nat),
-   Nplength a = ni n -> forall k:nat, k < n -> Nbit a k = false.
+   Nplength a = ni n -> forall k:nat, k < n -> N.testbit_nat a k = false.
 Proof.
   simple induction a; trivial.
   simple induction p. simple induction n. intros. inversion H1.
@@ -46,33 +46,33 @@ Proof.
   intros. simpl in H1. discriminate H1.
   simple induction k. trivial.
   generalize H0. case n. intros. inversion H3.
-  intros. simpl in |- *. unfold Nbit in H. apply (H n0). simpl in H1. inversion H1. reflexivity.
+  intros. simpl in |- *. unfold N.testbit_nat in H. apply (H n0). simpl in H1. inversion H1. reflexivity.
   exact (lt_S_n n1 n0 H3).
   simpl in |- *. intros n H. inversion H. intros. inversion H0.
 Qed.
 
 Lemma Nplength_one :
- forall (a:N) (n:nat), Nplength a = ni n -> Nbit a n = true.
+ forall (a:N) (n:nat), Nplength a = ni n -> N.testbit_nat a n = true.
 Proof.
   simple induction a. intros. inversion H.
   simple induction p. intros. simpl in H0. inversion H0. reflexivity.
-  intros. simpl in H0. inversion H0. simpl in |- *. unfold Nbit in H. apply H. reflexivity.
+  intros. simpl in H0. inversion H0. simpl in |- *. unfold N.testbit_nat in H. apply H. reflexivity.
   intros. simpl in H. inversion H. reflexivity.
 Qed.
 
 Lemma Nplength_first_one :
  forall (a:N) (n:nat),
-   (forall k:nat, k < n -> Nbit a k = false) ->
-   Nbit a n = true -> Nplength a = ni n.
+   (forall k:nat, k < n -> N.testbit_nat a k = false) ->
+   N.testbit_nat a n = true -> Nplength a = ni n.
 Proof.
   simple induction a. intros. simpl in H0. discriminate H0.
   simple induction p. intros. generalize H0. case n. intros. reflexivity.
-  intros. absurd (Nbit (Npos (xI p0)) 0 = false). trivial with bool.
+  intros. absurd (N.testbit_nat (Npos (xI p0)) 0 = false). trivial with bool.
   auto with bool arith.
   intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3.
   intros. simpl in |- *. unfold Nplength in H.
   cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity.
-  apply H. intros. change (Nbit (Npos (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4.
+  apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4.
   exact H3.
   intro. case n. trivial.
   intros. simpl in H0. discriminate H0.
@@ -222,27 +222,27 @@ Qed.
 
 Lemma Nplength_lb :
  forall (a:N) (n:nat),
-   (forall k:nat, k < n -> Nbit a k = false) -> ni_le (ni n) (Nplength a).
+   (forall k:nat, k < n -> N.testbit_nat a k = false) -> ni_le (ni n) (Nplength a).
 Proof.
   simple induction a. intros. exact (ni_min_inf_r (ni n)).
   intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial.
-  intro. absurd (Nbit (Npos p) (Pplength p) = false).
+  intro. absurd (N.testbit_nat (Npos p) (Pplength p) = false).
   rewrite
    (Nplength_one (Npos p) (Pplength p)
-      (refl_equal (Nplength (Npos p)))).
+      (eq_refl (Nplength (Npos p)))).
   discriminate.
   apply H. exact H0.
 Qed.
 
 Lemma Nplength_ub :
- forall (a:N) (n:nat), Nbit a n = true -> ni_le (Nplength a) (ni n).
+ forall (a:N) (n:nat), N.testbit_nat a n = true -> ni_le (Nplength a) (ni n).
 Proof.
   simple induction a. intros. discriminate H.
   intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial.
-  intro. absurd (Nbit (Npos p) n = true).
+  intro. absurd (N.testbit_nat (Npos p) n = true).
   rewrite
    (Nplength_zeros (Npos p) (Pplength p)
-      (refl_equal (Nplength (Npos p))) n H0).
+      (eq_refl (Nplength (Npos p))) n H0).
   discriminate.
   exact H.
 Qed.
@@ -255,26 +255,26 @@ Qed.
     Instead of working with $d$, we work with $pd$, namely
     [Npdist]: *)
 
-Definition Npdist (a a':N) := Nplength (Nxor a a').
+Definition Npdist (a a':N) := Nplength (N.lxor a a').
 
 (** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that
     $pd(a,a')=infty$ iff $a=a'$: *)
 
 Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty.
 Proof.
-  intros. unfold Npdist in |- *. rewrite Nxor_nilpotent. reflexivity.
+  intros. unfold Npdist in |- *. rewrite N.lxor_nilpotent. reflexivity.
 Qed.
 
 Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'.
 Proof.
-  intros. apply Nxor_eq. apply Nplength_infty. exact H.
+  intros. apply N.lxor_eq. apply Nplength_infty. exact H.
 Qed.
 
 (** $d$ is a distance, so $d(a,a')=d(a',a)$: *)
 
 Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a.
 Proof.
-  unfold Npdist in |- *. intros. rewrite Nxor_comm. reflexivity.
+  unfold Npdist in |- *. intros. rewrite N.lxor_comm. reflexivity.
 Qed.
 
 (** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq
@@ -292,21 +292,21 @@ Qed.
 Lemma Nplength_ultra_1 :
  forall a a':N,
    ni_le (Nplength a) (Nplength a') ->
-   ni_le (Nplength a) (Nplength (Nxor a a')).
+   ni_le (Nplength a) (Nplength (N.lxor a a')).
 Proof.
   simple induction a. intros. unfold ni_le in H. unfold Nplength at 1 3 in H.
   rewrite (ni_min_inf_l (Nplength a')) in H.
   rewrite (Nplength_infty a' H). simpl in |- *. apply ni_le_refl.
   intros. unfold Nplength at 1 in |- *. apply Nplength_lb. intros.
-  cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false).
+  cut (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false).
   intros. apply H1. reflexivity.
   intro a''. case a''. intro. reflexivity.
   intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k).
   rewrite
    (Nplength_zeros (Npos p) (Pplength p)
-      (refl_equal (Nplength (Npos p))) k H0).
+      (eq_refl (Nplength (Npos p))) k H0).
   generalize H. case a'. trivial.
-  intros. cut (Nbit (Npos p1) k = false). intros. rewrite H3. reflexivity.
+  intros. cut (N.testbit_nat (Npos p1) k = false). intros. rewrite H3. reflexivity.
   apply Nplength_zeros with (n := Pplength p1). reflexivity.
   apply (lt_le_trans k (Pplength p) (Pplength p1)). exact H0.
   apply ni_le_le. exact H2.
@@ -314,14 +314,14 @@ Qed.
 
 Lemma Nplength_ultra :
  forall a a':N,
-   ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (Nxor a a')).
+   ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')).
 Proof.
   intros. case (ni_le_total (Nplength a) (Nplength a')). intro.
   cut (ni_min (Nplength a) (Nplength a') = Nplength a).
   intro. rewrite H0. apply Nplength_ultra_1. exact H.
   exact H.
   intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a').
-  intro. rewrite H0. rewrite Nxor_comm. apply Nplength_ultra_1. exact H.
+  intro. rewrite H0. rewrite N.lxor_comm. apply Nplength_ultra_1. exact H.
   rewrite ni_min_comm. exact H.
 Qed.
 
@@ -329,8 +329,8 @@ Lemma Npdist_ultra :
  forall a a' a'':N,
    ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a').
 Proof.
-  intros. unfold Npdist in |- *. cut (Nxor (Nxor a a'') (Nxor a'' a') = Nxor a a').
+  intros. unfold Npdist in |- *. cut (N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a').
   intro. rewrite <- H. apply Nplength_ultra.
-  rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent.
-  rewrite Nxor_neutral_left. reflexivity.
+  rewrite N.lxor_assoc. rewrite <- (N.lxor_assoc a'' a'' a'). rewrite N.lxor_nilpotent.
+  rewrite N.lxor_0_l. reflexivity.
 Qed.