Modularization of BinNat + fixes of stdlib

 A sub-module N in BinNat now contains functions add (ex-Nplus),
 mul (ex-Nmult), ... and properties.

 In particular, this sub-module N directly instantiates NAxiomsSig
  and includes all derived properties NProp.

 Files Ndiv_def and co are now obsolete and kept only for compat

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

6 files changed, 1185 insertions, 979 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 3a4250566..b1d62d776 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -7,7 +7,8 @@
 (************************************************************************)
 
 Require Export BinNums.
-Require Import BinPos.
+Require Import BinPos RelationClasses Morphisms Setoid
+ Equalities GenericMinMax Wf_nat Bool NAxioms NProperties.
 
 (**********************************************************************)
 (** * Binary natural numbers, operations and properties *)
@@ -16,25 +17,35 @@ Require Import BinPos.
 (** The type [N] and its constructors [N0] and [Npos] are now
     defined in [BinNums.v] *)
 
+(** Every definitions and early properties about binary natural numbers
+    are placed in a module [N] for qualification purpose. *)
+
 Local Open Scope N_scope.
 
-Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }.
-Proof.
- destruct n; auto.
- left; exists p; auto.
-Defined.
+(** Every definitions and early properties about positive numbers
+    are placed in a module [N] for qualification purpose. *)
+
+Module N
+ <: NAxiomsMiniSig
+ <: UsualOrderedTypeFull
+ <: UsualDecidableTypeFull
+ <: TotalOrder.
+
+Definition t := N.
+Definition eq := @Logic.eq t.
+Definition eq_equiv := @eq_equivalence t.
 
-(** Operation x -> 2*x+1 *)
+(** Operation [x -> 2*x+1] *)
 
-Definition Ndouble_plus_one x :=
+Definition succ_double x :=
   match x with
   | 0 => Npos 1
   | Npos p => Npos p~1
   end.
 
-(** Operation x -> 2*x *)
+(** Operation [x -> 2*x] *)
 
-Definition Ndouble n :=
+Definition double n :=
   match n with
   | 0 => 0
   | Npos p => Npos p~0
@@ -42,88 +53,68 @@ Definition Ndouble n :=
 
 (** Successor *)
 
-Definition Nsucc n :=
+Definition succ n :=
   match n with
-  | 0 => Npos 1
-  | Npos p => Npos (Psucc p)
+  | 0 => 1
+  | Npos p => Npos (Pos.succ p)
   end.
 
 (** Predecessor *)
 
-Definition Npred (n : N) := match n with
-| 0 => 0
-| Npos p => match p with
-  | xH => 0
-  | _ => Npos (Ppred p)
-  end
-end.
+Definition pred n :=
+  match n with
+  | 0 => 0
+  | Npos p => Pos.pred_N p
+  end.
 
 (** The successor of a N can be seen as a positive *)
 
-Definition Nsucc_pos (n : N) : positive :=
+Definition succ_pos (n : N) : positive :=
  match n with
    | N0 => 1%positive
-   | Npos p => Psucc p
+   | Npos p => Pos.succ p
  end.
 
-(** Similarly, the predecessor of a positive, seen as a N *)
-
-Definition Ppred_N (p:positive) : N :=
- match p with
-   | 1 => N0
-   | p~1 => Npos (p~0)
-   | p~0 => Npos (Pdouble_minus_one p)
- end%positive.
-
 (** Addition *)
 
-Definition Nplus n m :=
+Definition add n m :=
   match n, m with
   | 0, _ => m
   | _, 0 => n
   | Npos p, Npos q => Npos (p + q)
   end.
 
-Infix "+" := Nplus : N_scope.
+Infix "+" := add : N_scope.
 
 (** Subtraction *)
 
-Definition Nminus (n m : N) :=
+Definition sub n m :=
 match n, m with
 | 0, _ => 0
 | n, 0 => n
 | Npos n', Npos m' =>
-  match Pminus_mask n' m' with
+  match Pos.sub_mask n' m' with
   | IsPos p => Npos p
   | _ => 0
   end
 end.
 
-Infix "-" := Nminus : N_scope.
+Infix "-" := sub : N_scope.
 
 (** Multiplication *)
 
-Definition Nmult n m :=
+Definition mul n m :=
   match n, m with
   | 0, _ => 0
   | _, 0 => 0
   | Npos p, Npos q => Npos (p * q)
   end.
 
-Infix "*" := Nmult : N_scope.
-
-(** Boolean Equality *)
-
-Definition Neqb n m :=
- match n, m with
-  | 0, 0 => true
-  | Npos n, Npos m => Peqb n m
-  | _,_ => false
- end.
+Infix "*" := mul : N_scope.
 
 (** Order *)
 
-Definition Ncompare n m :=
+Definition compare n m :=
   match n, m with
   | 0, 0 => Eq
   | 0, Npos m' => Lt
@@ -131,64 +122,299 @@ Definition Ncompare n m :=
   | Npos n', Npos m' => (n' ?= m')%positive
   end.
 
-Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
+Infix "?=" := compare (at level 70, no associativity) : N_scope.
 
-Definition Nlt (x y:N) := (x ?= y) = Lt.
-Definition Ngt (x y:N) := (x ?= y) = Gt.
-Definition Nle (x y:N) := (x ?= y) <> Gt.
-Definition Nge (x y:N) := (x ?= y) <> Lt.
+Definition lt x y := (x ?= y) = Lt.
+Definition gt x y := (x ?= y) = Gt.
+Definition le x y := (x ?= y) <> Gt.
+Definition ge x y := (x ?= y) <> Lt.
 
-Infix "<=" := Nle : N_scope.
-Infix "<" := Nlt : N_scope.
-Infix ">=" := Nge : N_scope.
-Infix ">" := Ngt : N_scope.
+Infix "<=" := le : N_scope.
+Infix "<" := lt : N_scope.
+Infix ">=" := ge : N_scope.
+Infix ">" := gt : N_scope.
 
 Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
 Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
 Notation "x < y < z" := (x < y /\ y < z) : N_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.
 
+(** Boolean equality and comparison *)
+
+(** Nota: this [eqb] is not convertible with the generated [N_beq],
+    since the underlying [Pos.eqb] differs from [positive_beq]
+    (cf BinIntDef). *)
+
+Fixpoint eqb n m :=
+  match n, m with
+    | 0, 0 => true
+    | Npos p, Npos q => Pos.eqb p q
+    | _, _ => false
+  end.
+
+Definition leb x y :=
+ match x ?= y with Gt => false | _ => true end.
+
+Definition ltb x y :=
+ match x ?= y with Lt => true | _ => false end.
+
+Infix "=?" := eqb (at level 70, no associativity) : N_scope.
+Infix "<=?" := leb (at level 70, no associativity) : N_scope.
+Infix "<?" := ltb (at level 70, no associativity) : N_scope.
+
 (** Min and max *)
 
-Definition Nmin (n n' : N) := match Ncompare n n' with
+Definition min n n' := match n ?= n' with
  | Lt | Eq => n
  | Gt => n'
  end.
 
-Definition Nmax (n n' : N) := match Ncompare n n' with
+Definition max n n' := match n ?= n' with
  | Lt | Eq => n'
  | Gt => n
  end.
 
+(** Dividing by 2 *)
+
+Definition div2 n :=
+  match n with
+  | 0 => 0
+  | Npos 1 => 0
+  | Npos (p~0) => Npos p
+  | Npos (p~1) => Npos p
+  end.
+
+(** Parity *)
+
+Definition even n :=
+  match n with
+    | 0 => true
+    | Npos (xO _) => true
+    | _ => false
+  end.
+
+Definition odd n := negb (even n).
+
+(** Power *)
+
+Definition pow n p :=
+  match p, n with
+    | 0, _ => Npos 1
+    | _, 0 => 0
+    | Npos p, Npos q => Npos (q^p)
+  end.
+
+Infix "^" := pow : N_scope.
+
+(** Base-2 logarithm *)
+
+Definition log2 n :=
+ match n with
+   | 0 => 0
+   | Npos 1 => 0
+   | Npos (p~0) => Npos (Pos.size p)
+   | Npos (p~1) => Npos (Pos.size p)
+ end.
+
+(** How many digits in a number ?
+    Number 0 is said to have no digits at all.
+*)
+
+Definition size n :=
+ match n with
+  | 0 => 0
+  | Npos p => Npos (Pos.size p)
+ end.
+
+Definition size_nat n :=
+ match n with
+  | 0 => O
+  | Npos p => Pos.size_nat p
+ end.
+
+(** Euclidean division *)
+
+Fixpoint pos_div_eucl (a:positive)(b:N) : N * N :=
+  match a with
+    | xH =>
+       match b with 1 => (1,0) | _ => (0,1) end
+    | xO a' =>
+       let (q, r) := pos_div_eucl a' b in
+       let r' := double r in
+       if b <=? r' then (succ_double q, r' - b)
+        else (double q, r')
+    | xI a' =>
+       let (q, r) := pos_div_eucl a' b in
+       let r' := succ_double r in
+       if b <=? r' then (succ_double q, r' - b)
+        else  (double q, r')
+  end.
+
+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
+  end.
+
+Definition div a b := fst (div_eucl a b).
+Definition modulo a b := snd (div_eucl a b).
+
+Infix "/" := div : N_scope.
+Infix "mod" := modulo (at level 40, no associativity) : N_scope.
+
+(** Greatest common divisor *)
+
+Definition divide p q := exists r, p*r = q.
+
+Notation "( p | q )" := (divide p q) (at level 0) : N_scope.
+
+Definition gcd a b :=
+ match a, b with
+  | 0, _ => b
+  | _, 0 => a
+  | Npos p, Npos q => Npos (Pos.gcd p q)
+ end.
+
+(** Generalized Gcd, also computing rests of [a] and [b] after
+    division by gcd. *)
+
+Definition ggcd a b :=
+ match a, b with
+  | 0, _ => (b,(0,1))
+  | _, 0 => (a,(1,0))
+  | Npos p, Npos q =>
+     let '(g,(aa,bb)) := Pos.ggcd p q in
+     (Npos g, (Npos aa, Npos bb))
+ end.
+
+(** Square root *)
+
+Definition sqrtrem n :=
+ match n with
+  | 0 => (0, 0)
+  | Npos p =>
+    match Pos.sqrtrem p with
+     | (s, IsPos r) => (Npos s, Npos r)
+     | (s, _) => (Npos s, 0)
+    end
+ end.
+
+Definition sqrt n :=
+ match n with
+  | 0 => 0
+  | Npos p => Npos (Pos.sqrt p)
+ end.
+
+(** Operation over bits of a [N] number. *)
+
+(** Logical [or] *)
+
+Definition lor n m :=
+ match n, m with
+   | 0, _ => m
+   | _, 0 => n
+   | Npos p, Npos q => Npos (Pos.lor p q)
+ end.
+
+(** Logical [and] *)
+
+Definition land n m :=
+ match n, m with
+  | 0, _ => 0
+  | _, 0 => 0
+  | Npos p, Npos q => Pos.land p q
+ end.
+
+(** Logical [diff] *)
+
+Fixpoint ldiff n m :=
+ match n, m with
+  | 0, _ => 0
+  | _, 0 => n
+  | Npos p, Npos q => Pos.ldiff p q
+ end.
+
+(** [xor] *)
+
+Definition lxor n m :=
+  match n, m with
+    | 0, _ => m
+    | _, 0 => n
+    | Npos p, Npos q => Pos.lxor p q
+  end.
+
+(** Shifts *)
+
+Definition shiftl_nat (a:N)(n:nat) := iter_nat n _ double a.
+
+Definition shiftr_nat (a:N)(n:nat) := iter_nat n _ div2 a.
+
+Definition shiftl a n :=
+  match a with
+    | 0 => 0
+    | Npos a => Npos (Pos.shiftl a n)
+  end.
+
+Definition shiftr a n :=
+  match n with
+    | 0 => a
+    | Npos p => Pos.iter p div2 a
+  end.
+
+(** Checking whether a particular bit is set or not *)
+
+Definition testbit_nat (a:N) :=
+  match a with
+    | 0 => fun _ => false
+    | Npos p => Pos.testbit_nat p
+  end.
+
+(** Same, but with index in N *)
+
+Definition testbit a n :=
+  match a with
+    | 0 => false
+    | Npos p => Pos.testbit p n
+  end.
+
 (** Translation from [N] to [nat] and back. *)
 
-Definition nat_of_N (a:N) :=
+Definition to_nat (a:N) :=
   match a with
   | N0 => O
-  | Npos p => nat_of_P p
+  | Npos p => Pos.to_nat p
   end.
 
-Definition N_of_nat (n:nat) :=
+Definition of_nat (n:nat) :=
   match n with
   | O => 0
-  | S n' => Npos (P_of_succ_nat n')
+  | S n' => Npos (Pos.of_succ_nat n')
   end.
 
 (** Decidability of equality. *)
 
-Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }.
+Definition eq_dec : forall n m : N, { n = m } + { n <> m }.
 Proof.
  decide equality.
- apply positive_eq_dec.
+ apply Pos.eq_dec.
 Defined.
 
-(** convenient induction principles *)
+(** Discrimination principle *)
 
-Lemma N_ind_double :
+Definition discr n : { p:positive | n = Npos p } + { n = N0 }.
+Proof.
+ destruct n; auto.
+ left; exists p; auto.
+Defined.
+
+(** Convenient induction principles *)
+
+Lemma binary_ind :
  forall (a:N) (P:N -> Prop),
    P 0 ->
-   (forall a, P a -> P (Ndouble a)) ->
-   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
+   (forall a, P a -> P (double a)) ->
+   (forall a, P a -> P (succ_double a)) -> P a.
 Proof.
  intros a P P0 P2 PS2. destruct a as [|p]. trivial.
  induction p as [p IHp|p IHp| ].
@@ -197,11 +423,11 @@ Proof.
  now apply (PS2 0).
 Qed.
 
-Lemma N_rec_double :
+Lemma binary_rec :
  forall (a:N) (P:N -> Set),
    P 0 ->
-   (forall a, P a -> P (Ndouble a)) ->
-   (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
+   (forall a, P a -> P (double a)) ->
+   (forall a, P a -> P (succ_double a)) -> P a.
 Proof.
  intros a P P0 P2 PS2. destruct a as [|p]. trivial.
  induction p as [p IHp|p IHp| ].
@@ -212,478 +438,996 @@ Qed.
 
 (** Peano induction on binary natural numbers *)
 
-Definition Nrect
+Definition peano_rect
   (P : N -> Type) (a : P 0)
-    (f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n :=
+    (f : forall n : N, P n -> P (succ n)) (n : N) : P n :=
 let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in
 let P' (p : positive) := P (Npos p) in
 match n return (P n) with
 | 0 => a
-| Npos p => Prect P' (f 0 a) f' p
+| Npos p => Pos.peano_rect P' (f 0 a) f' p
 end.
 
-Theorem Nrect_base : forall P a f, Nrect P a f 0 = a.
+Theorem peano_rect_base P a f : peano_rect P a f 0 = a.
 Proof.
-intros P a f; simpl; reflexivity.
+reflexivity.
 Qed.
 
-Theorem Nrect_step : forall P a f n, Nrect P a f (Nsucc n) = f n (Nrect P a f n).
+Theorem peano_rect_succ P a f n :
+ peano_rect P a f (succ n) = f n (peano_rect P a f n).
 Proof.
-intros P a f; destruct n as [| p]; simpl;
-[rewrite Prect_base | rewrite Prect_succ]; reflexivity.
+destruct n; simpl;
+[rewrite Pos.peano_rect_base | rewrite Pos.peano_rect_succ]; reflexivity.
 Qed.
 
-Definition Nind (P : N -> Prop) := Nrect P.
+Definition peano_ind (P : N -> Prop) := peano_rect P.
 
-Definition Nrec (P : N -> Set) := Nrect P.
+Definition peano_rec (P : N -> Set) := peano_rect P.
 
-Theorem Nrec_base : forall P a f, Nrec P a f 0 = a.
+Theorem peano_rec_base P a f : peano_rec P a f 0 = a.
 Proof.
-intros P a f; unfold Nrec; apply Nrect_base.
+apply peano_rect_base.
 Qed.
 
-Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n).
+Theorem peano_rec_succ P a f n :
+ peano_rec P a f (succ n) = f n (peano_rec P a f n).
 Proof.
-intros P a f; unfold Nrec; apply Nrect_step.
+apply peano_rect_succ.
 Qed.
 
-(** Properties of successor and predecessor *)
+(** Properties of double *)
 
-Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n.
+Lemma double_spec n : double n = 2 * n.
 Proof.
-intros [| p]; simpl. reflexivity.
-case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ).
-intro H; false_hyp H Psucc_not_one.
-Qed.
-
-Theorem Npred_minus : forall n, Npred n = Nminus n (Npos 1).
-Proof.
- intros [|[p|p|]]; trivial.
+ reflexivity.
 Qed.
 
-Lemma Nsucc_pred : forall n, n<>0 -> Nsucc (Npred n) = n.
+Lemma succ_double_spec n : succ_double n = 2 * n + 1.
 Proof.
- intros [|n] H; (now destruct H) || clear H.
- rewrite Npred_minus. simpl. destruct n; simpl; trivial.
- f_equal; apply Psucc_o_double_minus_one_eq_xO.
+ now destruct n.
 Qed.
 
 (** Properties of mixed successor and predecessor. *)
 
-Lemma Ppred_N_spec : forall p, Ppred_N p = Npred (Npos p).
+Lemma pos_pred_spec p : Pos.pred_N p = pred (Npos p).
 Proof.
  now destruct p.
 Qed.
 
-Lemma Nsucc_pos_spec : forall n, Npos (Nsucc_pos n) = Nsucc n.
+Lemma succ_pos_spec n : Npos (succ_pos n) = succ n.
 Proof.
  now destruct n.
 Qed.
 
-Lemma Ppred_Nsucc : forall n, Ppred_N (Nsucc_pos n) = n.
+Lemma pos_pred_succ n : Pos.pred_N (succ_pos n) = n.
 Proof.
- intros. now rewrite Ppred_N_spec, Nsucc_pos_spec, Npred_succ.
+ destruct n. trivial. apply Pos.pred_N_succ.
 Qed.
 
-(** Properties of addition *)
-
-Theorem Nplus_0_l : forall n:N, 0 + n = n.
+Lemma succ_pos_pred p : succ (Pos.pred_N p) = Npos p.
 Proof.
-reflexivity.
+ destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double.
 Qed.
 
-Theorem Nplus_0_r : forall n:N, n + 0 = n.
+(** Properties of successor and predecessor *)
+
+Theorem pred_succ n : pred (succ n) = n.
 Proof.
-destruct n; reflexivity.
+destruct n; trivial. simpl. apply Pos.pred_N_succ.
 Qed.
 
-Theorem Nplus_comm : forall n m:N, n + m = m + n.
+Theorem pred_sub n : pred n = sub n 1.
 Proof.
-intros.
-destruct n; destruct m; simpl; try reflexivity.
-rewrite Pplus_comm; reflexivity.
+ now destruct n as [|[p|p|]].
 Qed.
 
-Theorem Nplus_assoc : forall n m p:N, n + (m + p) = n + m + p.
+Theorem succ_0_discr n : succ n <> 0.
 Proof.
-intros.
-destruct n; try reflexivity.
-destruct m; try reflexivity.
-destruct p; try reflexivity.
-simpl; rewrite Pplus_assoc; reflexivity.
+now destruct n.
 Qed.
 
-Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m).
+(** Specification of addition *)
+
+Theorem add_0_l n : 0 + n = n.
 Proof.
-destruct n, m.
-  simpl; reflexivity.
-  unfold Nsucc, Nplus; rewrite <- Pplus_one_succ_l; reflexivity.
-  simpl; reflexivity.
-  simpl; rewrite Pplus_succ_permute_l; reflexivity.
+reflexivity.
 Qed.
 
-Theorem Nsucc_0 : forall n : N, Nsucc n <> 0.
+Theorem add_succ_l n m : succ n + m = succ (n + m).
 Proof.
-now destruct n.
+destruct n, m; unfold succ, add; now rewrite ?Pos.add_1_l, ?Pos.add_succ_l.
 Qed.
 
-Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m.
+(** Specification of subtraction. *)
+
+Theorem sub_0_r n : n - 0 = n.
 Proof.
-intros [|p] [|q] H; simpl in *; trivial; injection H; clear H; intro H.
-  now elim (Psucc_not_one q).
-  now elim (Psucc_not_one p).
-  apply Psucc_inj in H. now f_equal.
+now destruct n.
 Qed.
 
-Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p.
+Theorem sub_succ_r n m : n - succ m = pred (n - m).
 Proof.
- induction n using Nind.
-  trivial.
-  intros m p H; rewrite 2 Nplus_succ in H.
-  apply Nsucc_inj in H. now apply IHn.
+destruct n as [|p], m as [|q]; trivial.
+now destruct p.
+simpl. rewrite Pos.sub_mask_succ_r, Pos.sub_mask_carry_spec.
+now destruct (Pos.sub_mask p q) as [|[r|r|]|].
 Qed.
 
-(** Properties of subtraction. *)
+(** Specification of multiplication *)
 
-Lemma Nminus_N0_Nle : forall n n' : N, n - n' = 0 <-> n <= n'.
+Theorem mul_0_l n : 0 * n = 0.
 Proof.
-intros [| p] [| q]; unfold Nle; simpl;
-split; intro H; try easy.
-now elim H.
-contradict H. now destruct (Pminus_mask_Gt _ _ H) as (h & -> & _).
-destruct (Pcompare_spec p q); try now elim H.
-subst. now rewrite Pminus_mask_diag.
-now rewrite Pminus_mask_Lt.
+reflexivity.
 Qed.
 
-Theorem Nminus_0_r : forall n : N, n - 0 = n.
+Theorem mul_succ_l n m : (succ n) * m = n * m + m.
 Proof.
-now destruct n.
+destruct n, m; simpl; trivial. f_equal. rewrite Pos.add_comm.
+apply Pos.mul_succ_l.
 Qed.
 
-Theorem Nminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m).
+(** Properties of comparison *)
+
+Lemma compare_refl n : (n ?= n) = Eq.
 Proof.
-intros [|p] [|q]; trivial.
-now destruct p.
-simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
-now destruct (Pminus_mask p q) as [|[r|r|]|].
+destruct n; simpl; trivial. apply Pos.compare_refl.
 Qed.
 
-(** Properties of multiplication *)
+Theorem compare_eq n m : (n ?= m) = Eq -> n = m.
+Proof.
+destruct n, m; simpl; try easy. intros. f_equal.
+now apply Pos.compare_eq.
+Qed.
 
-Theorem Nmult_0_l : forall n:N, 0 * n = 0.
+Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
 Proof.
-reflexivity.
+split; intros. now apply compare_eq. subst; now apply compare_refl.
 Qed.
 
-Theorem Nmult_1_l : forall n:N, Npos 1 * n = n.
+Lemma compare_antisym n m : CompOpp (n ?= m) = (m ?= n).
 Proof.
-destruct n; reflexivity.
+destruct n, m; simpl; trivial.
+symmetry. apply Pos.compare_antisym. (* TODO : quel sens ? *)
 Qed.
 
-Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m.
+(** Specification of lt and le *)
+
+Theorem lt_irrefl n : ~ n < n.
 Proof.
-intros [|n] [|m]; simpl; trivial. now rewrite Pmult_Sn_m.
+unfold lt. now rewrite compare_refl.
 Qed.
 
-Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n.
+Lemma lt_eq_cases n m : n <= m <-> n < m \/ n=m.
 Proof.
-intros [|n]; simpl; trivial. now rewrite Pmult_1_r.
+unfold le, lt. rewrite <- compare_eq_iff.
+destruct (n ?= m); now intuition.
 Qed.
 
-Theorem Nmult_comm : forall n m:N, n * m = m * n.
+Lemma lt_succ_r n m : n < succ m <-> n<=m.
 Proof.
-intros [|n] [|m]; simpl; trivial. now rewrite Pmult_comm.
+destruct n as [|p], m as [|q]; simpl; try easy'.
+split. now destruct p. now destruct 1.
+apply Pos.lt_succ_r.
 Qed.
 
-Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p.
+Lemma compare_spec n m : CompareSpec (n=m) (n<m) (m<n) (n ?= m).
 Proof.
-intros.
-destruct n; try reflexivity.
-destruct m; try reflexivity.
-destruct p; try reflexivity.
-simpl; rewrite Pmult_assoc; reflexivity.
+case_eq (n ?= m); intro H; constructor; trivial.
+now apply compare_eq.
+red. now rewrite <- compare_antisym, H.
 Qed.
 
-Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p.
+(** Properties of boolean comparisons. *)
+
+Lemma eqb_eq n m : eqb n m = true <-> n=m.
 Proof.
-intros.
-destruct n; try reflexivity.
-destruct m; destruct p; try reflexivity.
-simpl; rewrite Pmult_plus_distr_r; reflexivity.
+destruct n as [|n], m as [|m]; simpl; try easy'.
+rewrite Pos.eqb_eq. split; intro H. now subst. now destr_eq H.
 Qed.
 
-Theorem Nmult_plus_distr_l : forall n m p:N, p * (n + m) = p * n + p * m.
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
 Proof.
-intros. rewrite ! (Nmult_comm p); apply Nmult_plus_distr_r.
+  unfold ltb, lt. destruct compare; easy'.
 Qed.
 
-Theorem Nmult_reg_r : forall n m p:N, p <> 0 -> n * p = m * p -> n = m.
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
 Proof.
-destruct p; intros Hp H.
-contradiction Hp; reflexivity.
-destruct n; destruct m; reflexivity || (try discriminate H).
-injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity.
+  unfold leb, le. destruct compare; easy'.
 Qed.
 
-(** Properties of boolean order. *)
+Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m).
+Proof.
+ unfold le, lt, leb. rewrite <- (compare_antisym n m).
+ case compare; now constructor.
+Qed.
 
-Lemma Neqb_eq : forall n m, Neqb n m = true <-> n=m.
+Lemma ltb_spec n m : BoolSpec (n<m) (m<=n) (n <? m).
 Proof.
-destruct n as [|n], m as [|m]; simpl; split; auto; try discriminate.
-intros; f_equal. apply (Peqb_eq n m); auto.
-intros. apply (Peqb_eq n m). congruence.
+ unfold le, lt, ltb. rewrite <- (compare_antisym n m).
+ case compare; now constructor.
 Qed.
 
-(** Properties of comparison *)
+(** We regroup here some results used for proving the correctness
+    of more advanced functions. These results will also be provided
+    by the generic functor of properties about natural numbers
+    instantiated at the end of the file. *)
+
+Module Import BootStrap.
 
-Lemma Nle_0 : forall n, 0<=n.
+Theorem succ_inj n m : succ n = succ m -> n = m.
 Proof.
- now destruct n.
+destruct n as [|p], m as [|q]; intro H; simpl in *; trivial; destr_eq H.
+ now destruct (Pos.succ_not_1 q).
+ now destruct (Pos.succ_not_1 p).
+ f_equal. now apply Pos.succ_inj.
 Qed.
 
-Lemma Ncompare_refl : forall n, (n ?= n) = Eq.
+Theorem add_0_r n : n + 0 = n.
 Proof.
-destruct n; simpl; auto.
-apply Pcompare_refl.
+now destruct n.
 Qed.
 
-Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m.
+Theorem add_comm n m : n + m = m + n.
 Proof.
-destruct n as [| n]; destruct m as [| m]; simpl; intro H;
- reflexivity || (try discriminate H).
-  rewrite (Pcompare_Eq_eq n m H); reflexivity.
+destruct n, m; simpl; try reflexivity. simpl. f_equal. apply Pos.add_comm.
 Qed.
 
-Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m.
+Theorem add_assoc n m p : n + (m + p) = n + m + p.
 Proof.
-split; intros;
- [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ].
+destruct n; try reflexivity.
+destruct m; try reflexivity.
+destruct p; try reflexivity.
+simpl. f_equal. apply Pos.add_assoc.
 Qed.
 
-Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n).
+Lemma sub_add n m : n <= m -> m - n + n = m.
 Proof.
-destruct n; destruct m; simpl; auto.
-exact (Pcompare_antisym p p0 Eq).
+ destruct n as [|p], m as [|q]; simpl; try easy'.
+ unfold le, compare. rewrite Pos.compare_antisym. intros H.
+ assert (H1 := Pos.sub_mask_compare q p).
+ assert (H2 := Pos.sub_mask_add q p).
+ destruct Pos.sub_mask as [|r|]; simpl in *; f_equal.
+ symmetry. now apply Pos.compare_eq.
+ rewrite Pos.add_comm. now apply H2.
+ rewrite <- H1 in H. now destruct H.
 Qed.
 
-Lemma Ngt_Nlt : forall n m, n > m -> m < n.
+Theorem mul_1_l n : 1 * n = n.
 Proof.
-unfold Ngt, Nlt; intros n m GT.
-rewrite <- Ncompare_antisym, GT; reflexivity.
+now destruct n.
 Qed.
 
-Theorem Nlt_irrefl : forall n : N, ~ n < n.
+Theorem mul_comm n m : n * m = m * n.
 Proof.
-intro n; unfold Nlt; now rewrite Ncompare_refl.
+destruct n, m; simpl; trivial. f_equal. apply Pos.mul_comm.
 Qed.
 
-Theorem Nlt_trans : forall n m q, n < m -> m < q -> n < q.
+Theorem mul_assoc n m p : n * (m * p) = n * m * p.
 Proof.
-destruct n;
- destruct m; try discriminate;
- destruct q; try discriminate; auto.
-eapply Plt_trans; eauto.
+destruct n; try reflexivity.
+destruct m; try reflexivity.
+destruct p; try reflexivity.
+simpl. f_equal. apply Pos.mul_assoc.
 Qed.
 
-Theorem Nlt_not_eq : forall n m, n < m -> ~ n = m.
+Theorem mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
 Proof.
- intros n m LT EQ. subst m. elim (Nlt_irrefl n); auto.
+destruct n; try reflexivity.
+destruct m, p; try reflexivity.
+simpl. f_equal. apply Pos.mul_add_distr_r.
 Qed.
 
-Theorem Ncompare_n_Sm :
-  forall n m : N, (n ?= Nsucc m) = Lt <-> (n ?= m) = Lt \/ n = m.
+Theorem mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
 Proof.
-intros [|p] [|q]; simpl; split; intros H; auto.
-destruct p; discriminate.
-destruct H; discriminate.
-apply Plt_succ_r, Ple_lteq in H. destruct H; subst; auto.
-apply Plt_succ_r, Ple_lteq. destruct H; [left|right]; congruence.
+rewrite !(mul_comm n); apply mul_add_distr_r.
 Qed.
 
-Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y.
+Lemma le_0_l n : 0<=n.
 Proof.
-unfold Nle, Nlt; intros.
-generalize (Ncompare_eq_correct x y).
-destruct (x ?= y); intuition; discriminate.
+now destruct n.
 Qed.
 
-Lemma Nlt_succ_r : forall n m,  n < Nsucc m <-> n<=m.
+Theorem lt_trans n m q : n < m -> m < q -> n < q.
 Proof.
-intros n m.
-eapply iff_trans. apply Ncompare_n_Sm. apply iff_sym, Nle_lteq.
+destruct n, m, q; try easy. eapply Pos.lt_trans; eauto.
 Qed.
 
-Lemma Nle_trans : forall n m p, n<=m -> m<=p -> n<=p.
+Lemma le_trans n m p : n<=m -> m<=p -> n<=p.
 Proof.
- intros n m p H H'.
- apply Nle_lteq. apply Nle_lteq in H. apply Nle_lteq in H'.
- destruct H, H'; subst; auto.
- left; now apply Nlt_trans with m.
+ rewrite 3 lt_eq_cases. intros [H|H] [H'|H']; subst;
+  (now right) || left; trivial.
+ now apply lt_trans with m.
 Qed.
 
-Lemma Nle_succ_l : forall n m, Nsucc n <= m <-> n < m.
+Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m.
 Proof.
- intros.
- unfold Nle, Nlt.
- rewrite <- 2 (Ncompare_antisym m).
- generalize (Nlt_succ_r m n). unfold Nle,Nlt.
- destruct Ncompare, Ncompare; simpl; intros (U,V);
-  intuition; now try discriminate V.
+ intro H. destruct p. simpl; auto.
+ destruct n; destruct m.
+ elim (lt_irrefl _ H).
+ red; auto.
+ rewrite add_0_r in H. simpl in H.
+ red in H. simpl in H.
+ elim (Pos.lt_not_add_l _ _ H).
+ now apply (Pos.add_lt_mono_l p).
 Qed.
 
-Lemma Ncompare_spec : forall x y, CompareSpec (x=y) (x<y) (y<x) (x ?= y).
+End BootStrap.
+
+(** Specification of minimum and maximum *)
+
+Theorem min_l n m : n <= m -> min n m = n.
 Proof.
-intros.
-destruct (Ncompare x y) as [ ]_eqn; constructor; auto.
-apply Ncompare_Eq_eq; auto.
-apply Ngt_Nlt; auto.
+unfold min, le. case compare; trivial. now destruct 1.
 Qed.
 
-(** Order and operations *)
+Theorem min_r n m : m <= n -> min n m = m.
+Proof.
+unfold min, le. rewrite <- compare_antisym.
+case compare_spec; trivial. now destruct 2.
+Qed.
 
-(** NB : Many more results will come from NBinary, the Number instantiation.
-    The next lemmas are useful for proving the correctness of
-    advanced functions.
-*)
+Theorem max_l n m : m <= n -> max n m = n.
+Proof.
+unfold max, le. rewrite <- compare_antisym.
+case compare_spec; auto. now destruct 2.
+Qed.
 
-Lemma Nplus_lt_cancel_l : forall n m p, p+n < p+m -> n<m.
+Theorem max_r n m : n <= m -> max n m = m.
 Proof.
- intros. destruct p. simpl; auto.
- destruct n; destruct m.
- elim (Nlt_irrefl _ H).
- red; auto.
- rewrite Nplus_0_r in H. simpl in H.
- red in H. simpl in H.
- elim (Plt_not_plus_l _ _ H).
- now apply (Pplus_lt_mono_l p).
+unfold max, le. case compare; trivial. now destruct 1.
 Qed.
 
 (** 0 is the least natural number *)
 
-Theorem Ncompare_0 : forall n : N, Ncompare n 0 <> Lt.
+Theorem compare_0_r n : (n ?= 0) <> Lt.
 Proof.
-destruct n; discriminate.
+now destruct n.
 Qed.
 
 (** Dividing by 2 *)
 
-Definition Ndiv2 (n:N) :=
-  match n with
-  | 0 => 0
-  | Npos 1 => 0
-  | Npos (p~0) => Npos p
-  | Npos (p~1) => Npos p
-  end.
-
-Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n.
+Lemma div2_double n : div2 (double n) = n.
 Proof.
-  destruct n; trivial.
+now destruct n.
 Qed.
 
-Lemma Ndouble_plus_one_div2 :
- forall n:N, Ndiv2 (Ndouble_plus_one n) = n.
+Lemma div2_succ_double n : div2 (succ_double n) = n.
 Proof.
-  destruct n; trivial.
+now destruct n.
 Qed.
 
-Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m.
+Lemma double_inj n m : double n = double m -> n = m.
 Proof.
-  intros. rewrite <- (Ndouble_div2 n). rewrite H. apply Ndouble_div2.
+intro H. rewrite <- (div2_double n), H. apply div2_double.
 Qed.
 
-Lemma Ndouble_plus_one_inj :
- forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m.
+Lemma succ_double_inj n m : succ_double n = succ_double m -> n = m.
 Proof.
-  intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2.
+intro H. rewrite <- (div2_succ_double n), H. apply div2_succ_double.
 Qed.
 
-(** Power *)
-
-Definition Npow n p :=
-  match p, n with
-    | 0, _ => Npos 1
-    | _, 0 => 0
-    | Npos p, Npos q => Npos (Ppow q p)
-  end.
-
-Infix "^" := Npow : N_scope.
+(** Speficications of power *)
 
-Lemma Npow_0_r : forall n, n ^ 0 = Npos 1.
+Lemma pow_0_r n : n ^ 0 = 1.
 Proof. reflexivity. Qed.
 
-Lemma Npow_succ_r : forall n p, n^(Nsucc p) = n * n^p.
+Lemma pow_succ_r n p : 0<=p -> n^(succ p) = n * n^p.
 Proof.
- intros [|q] [|p]; simpl; trivial; f_equal.
- apply Ppow_succ_r.
+ intros _.
+ destruct n, p; simpl; trivial; f_equal. apply Pos.pow_succ_r.
 Qed.
 
-(** Base-2 logarithm *)
+Lemma pow_neg_r n p : p<0 -> n^p = 0.
+Proof.
+ now destruct p.
+Qed.
 
-Definition Nlog2 n :=
- match n with
-   | 0 => 0
-   | Npos 1 => 0
-   | Npos (p~0) => Npos (Psize_pos p)
-   | Npos (p~1) => Npos (Psize_pos p)
- end.
+(** Specification of Base-2 logarithm *)
 
-Lemma Nlog2_spec : forall n, 0 < n ->
- (Npos 2)^(Nlog2 n) <= n < (Npos 2)^(Nsucc (Nlog2 n)).
+Lemma log2_spec n : 0 < n ->
+ 2^(log2 n) <= n < 2^(succ (log2 n)).
 Proof.
- intros [|[p|p|]] H; discriminate H || clear H; simpl; split.
- eapply Nle_trans with (Npos (p~0)).
- apply Psize_pos_le.
- apply Nle_lteq; left. exact (Pcompare_p_Sp (p~0)).
- apply Psize_pos_gt.
- apply Psize_pos_le.
- apply Psize_pos_gt.
+ destruct n as [|[p|p|]]; discriminate || intros _; simpl; split.
+ eapply le_trans with (Npos (p~0)).
+ apply Pos.size_le.
+ apply lt_eq_cases; left. apply Pos.lt_succ_diag_r.
+ apply Pos.size_gt.
+ apply Pos.size_le.
+ apply Pos.size_gt.
  discriminate.
  reflexivity.
 Qed.
 
-Lemma Nlog2_nonpos : forall n, n<=0 -> Nlog2 n = 0.
+Lemma log2_nonpos n : n<=0 -> log2 n = 0.
 Proof.
- intros [|n] Hn. reflexivity. now destruct Hn.
+ destruct n; intros Hn. reflexivity. now destruct Hn.
 Qed.
 
-(** Parity *)
+Lemma size_log2 n : n<>0 -> size n = succ (log2 n).
+Proof.
+ destruct n as [|[n|n| ]]; trivial. now destruct 1.
+Qed.
 
-Definition Neven n :=
-  match n with
-    | 0 => true
-    | Npos (xO _) => true
-    | _ => false
-  end.
-Definition Nodd n := negb (Neven n).
+Lemma size_gt n : n < 2^(size n).
+Proof.
+ destruct n. reflexivity. simpl. apply Pos.size_gt.
+Qed.
 
-Lemma Neven_spec : forall n, Neven n = true <-> exists m, n=2*m.
+Lemma size_le n : 2^(size n) <= succ_double n.
+Proof.
+ destruct n. discriminate.
+ simpl. apply le_trans with (Npos (p~0)).
+ apply Pos.size_le.
+ apply lt_eq_cases. left. apply Pos.lt_succ_diag_r.
+Qed.
+
+(** Specification of parity functions *)
+
+Definition Even n := exists m, n = 2*m.
+Definition Odd n := exists m, n = 2*m+1.
+
+Lemma even_spec n : even n = true <-> Even n.
 Proof.
  destruct n.
  split. now exists 0.
  trivial.
- destruct p; simpl; split; trivial; try discriminate.
+ destruct p; simpl; split; try easy.
  intros (m,H). now destruct m.
  now exists (Npos p).
  intros (m,H). now destruct m.
 Qed.
 
-Lemma Nodd_spec : forall n, Nodd n = true <-> exists m, n=2*m+1.
+Lemma odd_spec n : odd n = true <-> Odd n.
 Proof.
  destruct n.
  split. discriminate.
  intros (m,H). now destruct m.
- destruct p; simpl; split; trivial; try discriminate.
- exists (Npos p). reflexivity.
+ destruct p; simpl; split; try easy.
+ now exists (Npos p).
  intros (m,H). now destruct m.
- exists 0. reflexivity.
+ now exists 0.
+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.
+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).
+  assert (Npos a~1 = (double q)*b + succ_double r).
+   rewrite succ_double_spec, double_spec.
+   now rewrite add_assoc, <- mul_assoc, <- mul_add_distr_l, <- IHa.
+  case leb_spec; intros H'; trivial.
+  rewrite (succ_double_spec q), mul_add_distr_r, <- double_spec,
+   mul_1_l, <- add_assoc.
+  now rewrite (add_comm b), sub_add.
+  (* a~0 *)
+  destruct pos_div_eucl as (q,r).
+  assert (Npos a~0 = (double q)*b + double r).
+   rewrite (double_spec q), (double_spec r). (* BUG: !double_spec *)
+   now rewrite <- mul_assoc, <- mul_add_distr_l, <- IHa.
+  case leb_spec; intros H'; trivial.
+  rewrite (succ_double_spec q), mul_add_distr_r, <- double_spec,
+   mul_1_l, <- add_assoc.
+  now rewrite (add_comm b), sub_add.
+  (* 1 *)
+  now destruct b as [|[ | | ]].
+Qed.
+
+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)).
+  destruct pos_div_eucl. now rewrite mul_comm.
+Qed.
+
+Theorem div_mod' a b : a = b * (a/b) + (a mod b).
+Proof.
+  generalize (div_eucl_spec a b).
+  unfold div, modulo. now destruct div_eucl.
+Qed.
+
+Definition div_mod a b : b<>0 -> a = b * (a/b) + (a mod b).
+Proof.
+ intros _. apply div_mod'.
+Qed.
+
+Lemma succ_double_lt n m : n<m -> succ_double n < double m.
+Proof.
+ destruct n as [|n], m as [|m]; intros H; try easy.
+ unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, H.
+Qed.
+
+Theorem pos_div_eucl_remainder (a:positive) (b:N) :
+  b<>0 -> snd (pos_div_eucl a b) < b.
+Proof.
+  intros Hb.
+  induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.
+  (* a~1 *)
+  destruct pos_div_eucl as (q,r); simpl in *.
+  case leb_spec; intros H; simpl; trivial.
+  apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial.
+  destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].
+  apply (succ_double_lt _ _ IHa).
+  (* a~0 *)
+  destruct pos_div_eucl as (q,r); simpl in *.
+  case leb_spec; intros H; simpl; trivial.
+  apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial.
+  destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].
+  now destruct r.
+  (* 1 *)
+  destruct b as [|[ | | ]]; easy || (now destruct Hb).
+Qed.
+
+Theorem mod_lt a b : b<>0 -> a mod b < b.
+Proof.
+  destruct b as [ |b]. now destruct 1.
+  destruct a as [ |a]. reflexivity.
+  unfold modulo. simpl. apply pos_div_eucl_remainder.
+Qed.
+
+Theorem mod_bound_pos a b : 0<=a -> 0<b -> 0 <= a mod b < b.
+Proof.
+ intros _ H. split. apply le_0_l. apply mod_lt. now destruct b.
+Qed.
+
+(** Specification of square root *)
+
+Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.
+Proof.
+ destruct n. reflexivity.
+ unfold sqrtrem, sqrt, Pos.sqrt.
+ destruct (Pos.sqrtrem p) as (s,r). now destruct r.
+Qed.
+
+Lemma sqrtrem_spec n :
+ let (s,r) := sqrtrem n in n = s*s + r /\ r <= 2*s.
+Proof.
+ destruct n. now split.
+ generalize (Pos.sqrtrem_spec p). simpl.
+ destruct 1; simpl; subst; now split.
+Qed.
+
+Lemma sqrt_spec n : 0<=n ->
+ let s := sqrt n in s*s <= n < (succ s)*(succ s).
+Proof.
+ intros _. destruct n. now split. apply (Pos.sqrt_spec p).
+Qed.
+
+Lemma sqrt_neg n : n<0 -> sqrt n = 0.
+Proof.
+ now destruct n.
+Qed.
+
+(** Specification of gcd *)
+
+(** The first component of ggcd is gcd *)
+
+Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.
+Proof.
+ destruct a as [|p], b as [|q]; simpl; auto.
+ assert (H := Pos.ggcd_gcd p q).
+ destruct Pos.ggcd as (g,(aa,bb)); simpl; now f_equal.
+Qed.
+
+(** The other components of ggcd are indeed the correct factors. *)
+
+Lemma ggcd_correct_divisors a b :
+  let '(g,(aa,bb)) := ggcd a b in
+  a=g*aa /\ b=g*bb.
+Proof.
+ destruct a as [|p], b as [|q]; simpl; auto.
+ now rewrite Pos.mul_1_r.
+ now rewrite Pos.mul_1_r.
+ generalize (Pos.ggcd_correct_divisors p q).
+ destruct Pos.ggcd as (g,(aa,bb)); simpl.
+ destruct 1; split; now f_equal.
+Qed.
+
+(** We can use this fact to prove a part of the gcd correctness *)
+
+Lemma gcd_divide_l a b : (gcd a b | a).
+Proof.
+ rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
+ destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto.
+Qed.
+
+Lemma gcd_divide_r a b : (gcd a b | b).
+Proof.
+ rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
+ destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto.
+Qed.
+
+(** We now prove directly that gcd is the greatest amongst common divisors *)
+
+Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c|gcd a b).
+Proof.
+ destruct a as [ |p], b as [ |q]; simpl; trivial.
+ destruct c as [ |r]. intros (s,H). discriminate.
+ intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *.
+ 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.
+Qed.
+
+Lemma gcd_nonneg a b : 0 <= gcd a b.
+Proof. apply le_0_l. Qed.
+
+(** Specification of bitwise functions *)
+
+(** Correctness proofs for [testbit]. *)
+
+Lemma testbit_even_0 a : testbit (2*a) 0 = false.
+Proof.
+ now destruct a.
 Qed.
 
+Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
+Proof.
+ now destruct a.
+Qed.
+
+Lemma testbit_succ_r_div2 a n : 0<=n ->
+ testbit a (succ n) = testbit (div2 a) n.
+Proof.
+ intros _. destruct a as [|[a|a| ]], n as [|n]; simpl; trivial;
+  f_equal; apply Pos.pred_N_succ.
+Qed.
+
+Lemma testbit_odd_succ a n : 0<=n ->
+ testbit (2*a+1) (succ n) = testbit a n.
+Proof.
+ intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a.
+Qed.
+
+Lemma testbit_even_succ a n : 0<=n ->
+ testbit (2*a) (succ n) = testbit a n.
+Proof.
+ intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a.
+Qed.
+
+Lemma testbit_neg_r a n : n<0 -> testbit a n = false.
+Proof.
+ now destruct n.
+Qed.
+
+(** Correctness proofs for shifts *)
+
+Lemma shiftr_succ_r a n :
+ shiftr a (succ n) = div2 (shiftr a n).
+Proof.
+ destruct n; simpl; trivial. apply Pos.iter_succ.
+Qed.
+
+Lemma shiftl_succ_r a n :
+ shiftl a (succ n) = double (shiftl a n).
+Proof.
+ destruct n, a; simpl; trivial. f_equal. apply Pos.iter_succ.
+Qed.
+
+Lemma shiftr_spec a n m : 0<=m ->
+ testbit (shiftr a n) m = testbit a (m+n).
+Proof.
+ intros _. revert a m.
+ induction n using peano_ind; intros a m. now rewrite add_0_r.
+ rewrite add_comm, add_succ_l, add_comm, <- add_succ_l.
+ now rewrite <- IHn, testbit_succ_r_div2, shiftr_succ_r by apply le_0_l.
+Qed.
+
+Lemma shiftl_spec_high a n m : 0<=m -> n<=m ->
+ testbit (shiftl a n) m = testbit a (m-n).
+Proof.
+ intros _ H.
+ rewrite <- (sub_add n m H) at 1.
+ set (m' := m-n). clearbody m'. clear H m. revert a m'.
+ induction n using peano_ind; intros a m.
+ rewrite add_0_r; now destruct a.
+ rewrite shiftl_succ_r.
+ rewrite add_comm, add_succ_l, add_comm.
+ now rewrite testbit_succ_r_div2, div2_double by apply le_0_l.
+Qed.
+
+Lemma shiftl_spec_low a n m : m<n ->
+ testbit (shiftl a n) m = false.
+Proof.
+ revert a m.
+ induction n using peano_ind; intros a m H.
+ elim (le_0_l m). now rewrite <- compare_antisym, H.
+ rewrite shiftl_succ_r.
+ destruct m. now destruct (shiftl a n).
+ rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l.
+ apply IHn.
+ apply add_lt_cancel_l with 1. rewrite 2 (add_succ_l 0). simpl.
+ now rewrite succ_pos_pred.
+Qed.
+
+Definition div2_spec a : div2 a = shiftr a 1.
+Proof.
+ reflexivity.
+Qed.
+
+(** Semantics of bitwise operations *)
+
+Lemma pos_lxor_spec p p' n :
+ testbit (Pos.lxor p p') n = xorb (Pos.testbit p n) (Pos.testbit p' n).
+Proof.
+ revert p' n.
+ induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
+ (specialize (IH p'); destruct Pos.lxor; trivial; now rewrite <-IH) ||
+ (now destruct Pos.testbit).
+Qed.
+
+Lemma lxor_spec a a' n :
+ testbit (lxor a a') n = xorb (testbit a n) (testbit a' n).
+Proof.
+ destruct a, a'; simpl; trivial.
+ now destruct Pos.testbit.
+ now destruct Pos.testbit.
+ apply pos_lxor_spec.
+Qed.
+
+Lemma pos_lor_spec p p' n :
+ Pos.testbit (Pos.lor p p') n = (Pos.testbit p n) || (Pos.testbit p' n).
+Proof.
+ revert p' n.
+ induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
+  apply IH || now rewrite orb_false_r.
+Qed.
+
+Lemma lor_spec a a' n :
+ testbit (lor a a') n = (testbit a n) || (testbit a' n).
+Proof.
+ destruct a, a'; simpl; trivial.
+ now rewrite orb_false_r.
+ apply pos_lor_spec.
+Qed.
+
+Lemma pos_land_spec p p' n :
+ testbit (Pos.land p p') n = (Pos.testbit p n) && (Pos.testbit p' n).
+Proof.
+ revert p' n.
+ induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
+ (specialize (IH p'); destruct Pos.land; trivial; now rewrite <-IH) ||
+ (now rewrite andb_false_r).
+Qed.
+
+Lemma land_spec a a' n :
+ testbit (land a a') n = (testbit a n) && (testbit a' n).
+Proof.
+ destruct a, a'; simpl; trivial.
+ now rewrite andb_false_r.
+ apply pos_land_spec.
+Qed.
+
+Lemma pos_ldiff_spec p p' n :
+ testbit (Pos.ldiff p p') n = (Pos.testbit p n) && negb (Pos.testbit p' n).
+Proof.
+ revert p' n.
+ induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
+ (specialize (IH p'); destruct Pos.ldiff; trivial; now rewrite <-IH) ||
+ (now rewrite andb_true_r).
+Qed.
+
+Lemma ldiff_spec a a' n :
+ testbit (ldiff a a') n = (testbit a n) && negb (testbit a' n).
+Proof.
+ destruct a, a'; simpl; trivial.
+ now rewrite andb_true_r.
+ apply pos_ldiff_spec.
+Qed.
+
+(** Some constants *)
+
+Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
+
+Lemma one_succ : 1 = succ 0.
+Proof. reflexivity. Qed.
+
+Lemma two_succ : 2 = succ 1.
+Proof. reflexivity. Qed.
+
+Definition pred_0 : pred 0 = 0.
+Proof. reflexivity. Qed.
+
+(** Proof 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 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 pow_wd : Proper (eq==>eq==>eq) pow := _.
+Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+
+(** Generic induction / recursion *)
+
+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.
+Proof.
+intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS.
+Qed.
+
+Definition recursion {A} : A -> (N -> A -> A) -> N -> A :=
+  peano_rect (fun _ => A).
+
+Instance recursion_wd {A} (Aeq : relation A) :
+ Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion.
+Proof.
+intros a a' Ea f f' Ef x x' Ex. subst x'.
+induction x using peano_ind.
+trivial.
+unfold recursion in *. rewrite 2 peano_rect_succ. now apply Ef.
+Qed.
+
+Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a.
+Proof. reflexivity. Qed.
+
+Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A):
+ Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f ->
+  forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
+Proof.
+unfold recursion; intros a_wd f_wd n. induction n using peano_ind.
+rewrite peano_rect_succ. now apply f_wd.
+rewrite !peano_rect_succ in *. now apply f_wd.
+Qed.
+
+(** Instantiation of generic properties of natural numbers *)
+
+Include !NProp
+ <+ !UsualMinMaxLogicalProperties <+ !UsualMinMaxDecProperties.
+
+(* TODO : avoir un inlining selectif : t eq zero one two *)
+
+End N.
+
+(** Exportation of notations *)
+
+Infix "+" := N.add : N_scope.
+Infix "-" := N.sub : N_scope.
+Infix "*" := N.mul : N_scope.
+Infix "^" := N.pow : N_scope.
+
+Infix "?=" := N.compare (at level 70, no associativity) : N_scope.
+
+Infix "<=" := N.le : N_scope.
+Infix "<" := N.lt : N_scope.
+Infix ">=" := N.ge : N_scope.
+Infix ">" := N.gt : N_scope.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
+Notation "x < y < z" := (x < y /\ y < z) : N_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.
+
+Infix "=?" := N.eqb (at level 70, no associativity) : N_scope.
+Infix "<=?" := N.leb (at level 70, no associativity) : N_scope.
+Infix "<?" := N.ltb (at level 70, no associativity) : N_scope.
+
+Infix "/" := N.div : N_scope.
+Infix "mod" := N.modulo (at level 40, no associativity) : N_scope.
+
+Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope.
+
 (** Compatibility notations *)
 
-Notation N := N (only parsing).
+(*Notation N := N (only parsing).*) (*hidden by module N above *)
 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 Ndiscr := N.discr (only parsing).
+Notation Ndouble_plus_one := N.succ_double.
+Notation Ndouble := N.double (only parsing).
+Notation Nsucc := N.succ (only parsing).
+Notation Npred := N.pred (only parsing).
+Notation Nsucc_pos := N.succ_pos (only parsing).
+Notation Ppred_N := Pos.pred_N (only parsing).
+Notation Nplus := N.add (only parsing).
+Notation Nminus := N.sub (only parsing).
+Notation Nmult := N.mul (only parsing).
+Notation Neqb := N.eqb (only parsing).
+Notation Ncompare := N.compare (only parsing).
+Notation Nlt := N.lt (only parsing).
+Notation Ngt := N.gt (only parsing).
+Notation Nle := N.le (only parsing).
+Notation Nge := N.ge (only parsing).
+Notation Nmin := N.min (only parsing).
+Notation Nmax := N.max (only parsing).
+Notation Ndiv2 := N.div2 (only parsing).
+Notation Neven := N.even (only parsing).
+Notation Nodd := N.odd (only parsing).
+Notation Npow := N.pow (only parsing).
+Notation Nlog2 := N.log2 (only parsing).
+
+Notation nat_of_N := N.to_nat (only parsing).
+Notation N_of_nat := N.of_nat (only parsing).
+Notation N_eq_dec := N.eq_dec (only parsing).
+Notation N_ind_double := N.binary_ind (only parsing).
+Notation N_rec_double := N.binary_rec (only parsing).
+Notation Nrect := N.peano_rect (only parsing).
+Notation Nrect_base := N.peano_rect_base (only parsing).
+Notation Nrect_step := N.peano_rect_succ (only parsing).
+Notation Nind := N.peano_ind (only parsing).
+Notation Nrec := N.peano_rec (only parsing).
+Notation Nrec_base := N.peano_rec_base (only parsing).
+Notation Nrec_succ := N.peano_rec_succ (only parsing).
+
+Notation Npred_succ := N.pred_succ (only parsing).
+Notation Npred_minus := N.pred_sub (only parsing).
+Notation Nsucc_pred := N.succ_pred (only parsing).
+Notation Ppred_N_spec := N.pos_pred_spec (only parsing).
+Notation Nsucc_pos_spec := N.succ_pos_spec (only parsing).
+Notation Ppred_Nsucc := N.pos_pred_succ (only parsing).
+Notation Nplus_0_l := N.add_0_l (only parsing).
+Notation Nplus_0_r := N.add_0_r (only parsing).
+Notation Nplus_comm := N.add_comm (only parsing).
+Notation Nplus_assoc := N.add_assoc (only parsing).
+Notation Nplus_succ := N.add_succ_l (only parsing).
+Notation Nsucc_0 := N.succ_0_discr (only parsing).
+Notation Nsucc_inj := N.succ_inj (only parsing).
+Notation Nminus_N0_Nle := N.sub_0_le (only parsing).
+Notation Nminus_0_r := N.sub_0_r (only parsing).
+Notation Nminus_succ_r:= N.sub_succ_r (only parsing).
+Notation Nmult_0_l := N.mul_0_l (only parsing).
+Notation Nmult_1_l := N.mul_1_l (only parsing).
+Notation Nmult_1_r := N.mul_1_r (only parsing).
+Notation Nmult_comm := N.mul_comm (only parsing).
+Notation Nmult_assoc := N.mul_assoc (only parsing).
+Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing).
+Notation Neqb_eq := N.eqb_eq (only parsing).
+Notation Nle_0 := N.le_0_l (only parsing).
+Notation Ncompare_refl := N.compare_refl (only parsing).
+Notation Ncompare_Eq_eq := N.compare_eq (only parsing).
+Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing).
+Notation Ncompare_antisym := N.compare_antisym (only parsing).
+Notation Nlt_irrefl := N.lt_irrefl (only parsing).
+Notation Nlt_trans := N.lt_trans (only parsing).
+Notation Nle_lteq := N.lt_eq_cases (only parsing).
+Notation Nlt_succ_r := N.lt_succ_r (only parsing).
+Notation Nle_trans := N.le_trans (only parsing).
+Notation Nle_succ_l := N.le_succ_l (only parsing).
+Notation Ncompare_spec := N.compare_spec (only parsing).
+Notation Ncompare_0 := N.compare_0_r (only parsing).
+Notation Ndouble_div2 := N.div2_double (only parsing).
+Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing).
+Notation Ndouble_inj := N.double_inj (only parsing).
+Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing).
+Notation Npow_0_r := N.pow_0_r (only parsing).
+Notation Npow_succ_r := N.pow_succ_r (only parsing).
+Notation Nlog2_spec := N.log2_spec (only parsing).
+Notation Nlog2_nonpos := N.log2_nonpos (only parsing).
+Notation Neven_spec := N.even_spec (only parsing).
+Notation Nodd_spec := N.odd_spec (only parsing).
+Notation Nlt_not_eq := N.lt_neq (only parsing).
+
+(** More complex compatibility facts, expressed as lemmas
+    (to preserve scopes for instance) *)
+
+Lemma Nplus_reg_l n m p : n + m = n + p -> m = p.
+Proof (proj1 (N.add_cancel_l m p n)).
+Lemma Nmult_Sn_m n m : N.succ n * m = m + n * m.
+Proof (eq_trans (N.mul_succ_l n m) (N.add_comm _ _)).
+Lemma Nmult_plus_distr_l n m p : p * (n + m) = p * n + p * m.
+Proof (N.mul_add_distr_l p n m).
+Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
+Proof (fun H => proj1 (N.mul_cancel_r n m p H)).
+
+Lemma Ngt_Nlt n m : n > m -> m < n.
+Proof.
+unfold Ngt, Nlt; intro H. now rewrite <- N.compare_antisym, H.
+Qed.
+
+(** Not kept : Ncompare_n_Sm Nplus_lt_cancel_l *)
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 6bfc323d6..4a5f4ee1d 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -17,11 +17,6 @@ Require Export Nsqrt_def.
 Require Export Ngcd_def.
 Require Export Ndigits.
 Require Export NArithRing.
-Require NBinary.
-
-Module N.
- Include NBinary.N.
-End N.
 
 (** [N] contains an [order] tactic for natural numbers *)
 
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 94432a7cf..e13d6ac51 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -7,172 +7,38 @@
 (************************************************************************)
 
 Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat
- Pnat Nnat Ndiv_def Compare_dec Lt Minus.
+ Pnat Nnat Compare_dec Lt Minus.
 
-Local Open Scope positive_scope.
-
-(** Operation over bits of a [N] number. *)
-
-(** Logical [or] *)
-
-Fixpoint Por (p q : positive) : positive :=
-  match p, q with
-    | 1, q~0 => q~1
-    | 1, _ => q
-    | p~0, 1 => p~1
-    | _, 1 => p
-    | p~0, q~0 => (Por p q)~0
-    | p~0, q~1 => (Por p q)~1
-    | p~1, q~0 => (Por p q)~1
-    | p~1, q~1 => (Por p q)~1
-  end.
-
-Definition Nor n m :=
- match n, m with
-   | N0, _ => m
-   | _, N0 => n
-   | Npos p, Npos q => Npos (Por p q)
- end.
-
-(** Logical [and] *)
-
-Fixpoint Pand (p q : positive) : N :=
-  match p, q with
-    | 1, q~0 => N0
-    | 1, _ => Npos 1
-    | p~0, 1 => N0
-    | _, 1 => Npos 1
-    | p~0, q~0 => Ndouble (Pand p q)
-    | p~0, q~1 => Ndouble (Pand p q)
-    | p~1, q~0 => Ndouble (Pand p q)
-    | p~1, q~1 => Ndouble_plus_one (Pand p q)
-  end.
-
-Definition Nand n m :=
- match n, m with
-  | N0, _ => N0
-  | _, N0 => N0
-  | Npos p, Npos q => Pand p q
- end.
-
-(** Logical [diff] *)
-
-Fixpoint Pdiff (p q:positive) : N :=
-  match p, q with
-    | 1, q~0 => Npos 1
-    | 1, _ => N0
-    | _~0, 1 => Npos p
-    | p~1, 1 => Npos (p~0)
-    | p~0, q~0 => Ndouble (Pdiff p q)
-    | p~0, q~1 => Ndouble (Pdiff p q)
-    | p~1, q~1 => Ndouble (Pdiff p q)
-    | p~1, q~0 => Ndouble_plus_one (Pdiff p q)
-  end.
-
-Fixpoint Ndiff n m :=
- match n, m with
-  | N0, _ => N0
-  | _, N0 => n
-  | Npos p, Npos q => Pdiff p q
- end.
-
-(** [xor] *)
-
-Fixpoint Pxor (p q:positive) : N :=
-  match p, q with
-    | 1, 1 => N0
-    | 1, q~0 => Npos (q~1)
-    | 1, q~1 => Npos (q~0)
-    | p~0, 1 => Npos (p~1)
-    | p~0, q~0 => Ndouble (Pxor p q)
-    | p~0, q~1 => Ndouble_plus_one (Pxor p q)
-    | p~1, 1 => Npos (p~0)
-    | p~1, q~0 => Ndouble_plus_one (Pxor p q)
-    | p~1, q~1 => Ndouble (Pxor p q)
-  end.
-
-Definition Nxor (n m:N) :=
-  match n, m with
-    | N0, _ => m
-    | _, N0 => n
-    | Npos p, Npos q => Pxor p q
-  end.
-
-(** For proving properties of these operations, we will use
-  an equivalence with functional streams of bit, cf [eqf] below *)
-
-(** Shift *)
-
-Definition Nshiftl_nat (a:N)(n:nat) := iter_nat n _ Ndouble a.
-
-Definition Nshiftr_nat (a:N)(n:nat) := iter_nat n _ Ndiv2 a.
-
-Definition Nshiftr a n :=
-  match n with
-    | N0 => a
-    | Npos p => iter_pos p _ Ndiv2 a
-  end.
-
-Definition Nshiftl a n :=
-  match a, n with
-    | _, N0 => a
-    | N0, _ => a
-    | Npos p, Npos q => Npos (iter_pos q _ xO p)
-  end.
-
-(** Checking whether a particular bit is set on not *)
-
-Fixpoint Pbit (p:positive) : nat -> bool :=
-  match p with
-    | 1 => fun n => match n with
-                      | O => true
-                      | S _ => false
-                    end
-    | p~0 => fun n => match n with
-                        | O => false
-                        | S n' => Pbit p n'
-                      end
-    | p~1 => fun n => match n with
-                        | O => true
-                        | S n' => Pbit p n'
-                      end
-  end.
-
-Definition Nbit (a:N) :=
-  match a with
-    | N0 => fun _ => false
-    | Npos p => Pbit p
-  end.
-
-(** Same, but with index in N *)
+Local Open Scope N_scope.
 
-Fixpoint Ptestbit p n :=
-  match p, n with
-    | p~0, N0 => false
-    | _, N0 => true
-    | 1, _ => false
-    | p~0, _ => Ptestbit p (Npred n)
-    | p~1, _ => Ptestbit p (Npred n)
-  end.
+(** This file is mostly obsolete, see directly [BinNat] now. *)
 
-Definition Ntestbit a n :=
-  match a with
-    | N0 => false
-    | Npos p => Ptestbit p n
-  end.
+(** Operation over bits of a [N] number. *)
 
-Local Close Scope positive_scope.
-Local Open Scope N_scope.
+Notation Por := Pos.lor (only parsing).
+Notation Nor := N.lor (only parsing).
+Notation Pand := Pos.land (only parsing).
+Notation Nand := N.land (only parsing).
+Notation Pdiff := Pos.ldiff (only parsing).
+Notation Ndiff := N.ldiff (only parsing).
+Notation Pxor := Pos.lxor (only parsing).
+Notation Nxor := N.lxor (only parsing).
+Notation Nshiftl_nat := N.shiftl_nat (only parsing).
+Notation Nshiftr_nat := N.shiftr_nat (only parsing).
+Notation Nshiftl := N.shiftl (only parsing).
+Notation Nshiftr := N.shiftr (only parsing).
+Notation Pbit := Pos.testbit_nat (only parsing).
+Notation Nbit := N.testbit_nat (only parsing).
+Notation Ptestbit := Pos.testbit (only parsing).
+Notation Ntestbit := N.testbit (only parsing).
 
 (** Equivalence of Pbit and Ptestbit *)
 
 Lemma Ptestbit_Pbit :
  forall p n, Ptestbit p (N_of_nat n) = Pbit p n.
 Proof.
- induction p as [p IH|p IH| ]; intros n; simpl.
- rewrite <- N_of_pred, IH; destruct n; trivial.
- rewrite <- N_of_pred, IH; destruct n; trivial.
- destruct n; trivial.
+ 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.
 Qed.
 
 Lemma Ntestbit_Nbit : forall a n, Ntestbit a (N_of_nat n) = Nbit a n.
@@ -192,32 +58,6 @@ Proof.
  destruct a. trivial. apply Pbit_Ptestbit.
 Qed.
 
-(** Correctness proofs for [Ntestbit]. *)
-
-Lemma Ntestbit_odd_0 a : Ntestbit (2*a+1) 0 = true.
-Proof.
- now destruct a.
-Qed.
-
-Lemma Ntestbit_even_0 a : Ntestbit (2*a) 0 = false.
-Proof.
- now destruct a.
-Qed.
-
-Lemma Ntestbit_odd_succ a n :
- Ntestbit (2*a+1) (Nsucc n) = Ntestbit a n.
-Proof.
- destruct a. simpl. now destruct n.
- simpl. rewrite Npred_succ. now destruct n.
-Qed.
-
-Lemma Ntestbit_even_succ a n :
- Ntestbit (2*a) (Nsucc n) = Ntestbit a n.
-Proof.
- destruct a. trivial.
- simpl. rewrite Npred_succ. now destruct n.
-Qed.
-
 (** Equivalence of shifts, N and nat versions *)
 
 Lemma Nshiftr_nat_S : forall a n,
@@ -260,7 +100,7 @@ Proof.
  intros. now rewrite <- Nshiftl_nat_equiv, nat_of_N_of_nat.
 Qed.
 
-(** Correctness proofs for shifts *)
+(** Correctness proofs for shifts, nat version *)
 
 Lemma Nshiftr_nat_spec : forall a n m,
   Nbit (Nshiftr_nat a n) m = Nbit a (m+n).
@@ -271,14 +111,6 @@ Proof.
  destruct (Nshiftr_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
-Lemma Nshiftr_spec : forall a n m,
- Ntestbit (Nshiftr a n) m = Ntestbit a (m+n).
-Proof.
- intros.
- rewrite <- Nshiftr_nat_equiv, <- !Nbit_Ntestbit, nat_of_Nplus.
- apply Nshiftr_nat_spec.
-Qed.
-
 Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
   Nbit (Nshiftl_nat a n) m = Nbit a (m-n).
 Proof.
@@ -289,15 +121,6 @@ Proof.
  destruct (Nshiftl_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
-Lemma Nshiftl_spec_high : forall a n m, n<=m ->
- Ntestbit (Nshiftl a n) m = Ntestbit a (m-n).
-Proof.
- intros.
- rewrite <- Nshiftl_nat_equiv, <- !Nbit_Ntestbit, nat_of_Nminus.
- apply Nshiftl_nat_spec_high.
- apply nat_compare_le. now rewrite <- nat_of_Ncompare.
-Qed.
-
 Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
  Nbit (Nshiftl_nat a n) m = false.
 Proof.
@@ -309,18 +132,9 @@ Proof.
  destruct (Nshiftl_nat a n); trivial.
 Qed.
 
-Lemma Nshiftl_spec_low : forall a n m, m<n ->
- Ntestbit (Nshiftl a n) m = false.
-Proof.
- intros.
- rewrite <- Nshiftl_nat_equiv, <- Nbit_Ntestbit.
- apply Nshiftl_nat_spec_low.
- apply nat_compare_lt. now rewrite <- nat_of_Ncompare.
-Qed.
-
 (** A left shift for positive numbers (used in BigN) *)
 
-Definition Pshiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p.
+Notation Pshiftl_nat := Pos.shiftl_nat (only parsing).
 
 Lemma Pshiftl_nat_0 : forall p, Pshiftl_nat p 0 = p.
 Proof. reflexivity. Qed.
@@ -343,7 +157,7 @@ Proof.
  rewrite 2 Pshiftl_nat_S. now f_equal.
 Qed.
 
-(** Semantics of bitwise operations *)
+(** Semantics of bitwise operations with respect to [Nbit] *)
 
 Lemma Pxor_semantics : forall p p' n,
  Nbit (Pxor p p') n = xorb (Pbit p n) (Pbit p' n).
@@ -362,12 +176,6 @@ Proof.
  apply Pxor_semantics.
 Qed.
 
-Lemma Nxor_spec : forall a a' n,
- Ntestbit (Nxor a a') n = xorb (Ntestbit a n) (Ntestbit a' n).
-Proof.
- intros. rewrite <- !Nbit_Ntestbit. apply Nxor_semantics.
-Qed.
-
 Lemma Por_semantics : forall p p' n,
  Pbit (Por p p') n = (Pbit p n) || (Pbit p' n).
 Proof.
@@ -383,12 +191,6 @@ Proof.
  apply Por_semantics.
 Qed.
 
-Lemma Nor_spec : forall a a' n,
- Ntestbit (Nor a a') n = (Ntestbit a n) || (Ntestbit a' n).
-Proof.
- intros. rewrite <- !Nbit_Ntestbit. apply Nor_semantics.
-Qed.
-
 Lemma Pand_semantics : forall p p' n,
  Nbit (Pand p p') n = (Pbit p n) && (Pbit p' n).
 Proof.
@@ -405,12 +207,6 @@ Proof.
  apply Pand_semantics.
 Qed.
 
-Lemma Nand_spec : forall a a' n,
- Ntestbit (Nand a a') n = (Ntestbit a n) && (Ntestbit a' n).
-Proof.
- intros. rewrite <- !Nbit_Ntestbit. apply Nand_semantics.
-Qed.
-
 Lemma Pdiff_semantics : forall p p' n,
  Nbit (Pdiff p p') n = (Pbit p n) && negb (Pbit p' n).
 Proof.
@@ -427,12 +223,6 @@ Proof.
  apply Pdiff_semantics.
 Qed.
 
-Lemma Ndiff_spec : forall a a' n,
- Ntestbit (Ndiff a a') n = (Ntestbit a n) && negb (Ntestbit a' n).
-Proof.
- intros. rewrite <- !Nbit_Ntestbit. apply Ndiff_semantics.
-Qed.
-
 
 (** Equality over functional streams of bits *)
 
@@ -484,162 +274,67 @@ Ltac bitwise_semantics :=
 (** Now, we can easily deduce properties of [Nxor] and others
     from properties of [xorb] and others. *)
 
-Lemma Nxor_eq : forall a a', Nxor a a' = 0 -> a = a'.
-Proof.
- intros a a' H. bitwise_semantics. apply xorb_eq.
- now rewrite <- Nxor_semantics, H.
-Qed.
+Definition Nxor_eq : forall a a', Nxor a a' = 0 -> a = a' := N.lxor_eq.
+Definition Nxor_nilpotent : forall a, Nxor a a = 0 := N.lxor_nilpotent.
+Definition Nxor_0_l : forall n, Nxor 0 n = n := N.lxor_0_l.
+Definition Nxor_0_r : forall n, Nxor n 0 = n := N.lxor_0_r.
 
-Lemma Nxor_nilpotent : forall a, Nxor a a = 0.
-Proof.
- intros. bitwise_semantics. apply xorb_nilpotent.
-Qed.
-
-Lemma Nxor_0_l : forall n, Nxor 0 n = n.
-Proof.
- trivial.
-Qed.
 Notation Nxor_neutral_left := Nxor_0_l (only parsing).
-
-Lemma Nxor_0_r : forall n, Nxor n 0 = n.
-Proof.
- destruct n; trivial.
-Qed.
 Notation Nxor_neutral_right := Nxor_0_r (only parsing).
 
-Lemma Nxor_comm : forall a a', Nxor a a' = Nxor a' a.
-Proof.
- intros. bitwise_semantics. apply xorb_comm.
-Qed.
-
-Lemma Nxor_assoc :
- forall a a' a'', Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'').
-Proof.
- intros. bitwise_semantics. apply xorb_assoc.
-Qed.
-
-Lemma Nor_0_l : forall n, Nor 0 n = n.
-Proof.
- trivial.
-Qed.
-
-Lemma Nor_0_r : forall n, Nor n 0 = n.
-Proof.
- destruct n; trivial.
-Qed.
-
-Lemma Nor_comm : forall a a', Nor a a' = Nor a' a.
-Proof.
- intros. bitwise_semantics. apply orb_comm.
-Qed.
-
-Lemma Nor_assoc :
- forall a a' a'', Nor a (Nor a' a'') = Nor (Nor a a') a''.
-Proof.
- intros. bitwise_semantics. apply orb_assoc.
-Qed.
-
-Lemma Nor_diag : forall a, Nor a a = a.
-Proof.
- intros. bitwise_semantics. apply orb_diag.
-Qed.
-
-Lemma Nand_0_l : forall n, Nand 0 n = 0.
-Proof.
- trivial.
-Qed.
-
-Lemma Nand_0_r : forall n, Nand n 0 = 0.
-Proof.
- destruct n; trivial.
-Qed.
-
-Lemma Nand_comm : forall a a', Nand a a' = Nand a' a.
-Proof.
- intros. bitwise_semantics. apply andb_comm.
-Qed.
-
-Lemma Nand_assoc :
- forall a a' a'', Nand a (Nand a' a'') = Nand (Nand a a') a''.
-Proof.
- intros. bitwise_semantics. apply andb_assoc.
-Qed.
-
-Lemma Nand_diag : forall a, Nand a a = a.
-Proof.
- intros. bitwise_semantics. apply andb_diag.
-Qed.
-
-Lemma Ndiff_0_l : forall n, Ndiff 0 n = 0.
-Proof.
- trivial.
-Qed.
-
-Lemma Ndiff_0_r : forall n, Ndiff n 0 = n.
-Proof.
- destruct n; trivial.
-Qed.
-
-Lemma Ndiff_diag : forall a, Ndiff a a = 0.
-Proof.
- intros. bitwise_semantics. apply andb_negb_r.
-Qed.
-
-Lemma Nor_and_distr_l : forall a b c,
- Nor (Nand a b) c = Nand (Nor a c) (Nor b c).
-Proof.
- intros. bitwise_semantics. apply orb_andb_distrib_l.
-Qed.
-
-Lemma Nor_and_distr_r : forall a b c,
- Nor a (Nand b c) = Nand (Nor a b) (Nor a c).
-Proof.
- intros. bitwise_semantics. apply orb_andb_distrib_r.
-Qed.
-
-Lemma Nand_or_distr_l : forall a b c,
- Nand (Nor a b) c = Nor (Nand a c) (Nand b c).
-Proof.
- intros. bitwise_semantics. apply andb_orb_distrib_l.
-Qed.
-
-Lemma Nand_or_distr_r : forall a b c,
- Nand a (Nor b c) = Nor (Nand a b) (Nand a c).
-Proof.
- intros. bitwise_semantics. apply andb_orb_distrib_r.
-Qed.
-
-Lemma Ndiff_diff_l : forall a b c,
- Ndiff (Ndiff a b) c = Ndiff a (Nor b c).
-Proof.
- intros. bitwise_semantics. now rewrite negb_orb, andb_assoc.
-Qed.
-
-Lemma Nor_diff_and : forall a b,
- Nor (Ndiff a b) (Nand a b) = a.
-Proof.
- intros. bitwise_semantics.
- now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r.
-Qed.
-
-Lemma Nand_diff : forall a b,
- Nand (Ndiff a b) b = 0.
-Proof.
- intros. bitwise_semantics.
- now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r.
-Qed.
+Definition Nxor_comm : forall a a', Nxor a a' = Nxor a' a := N.lxor_comm.
+
+Definition Nxor_assoc :
+ forall a a' a'', Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'')
+ := N.lxor_assoc.
+
+Definition Nor_0_l : forall n, Nor 0 n = n := N.lor_0_l.
+Definition Nor_0_r : forall n, Nor n 0 = n := N.lor_0_r.
+Definition Nor_comm : forall a a', Nor a a' = Nor a' a := N.lor_comm.
+Definition Nor_assoc :
+ forall a a' a'', Nor a (Nor a' a'') = Nor (Nor a a') a''
+ := N.lor_assoc.
+Definition Nor_diag : forall a, Nor a a = a := N.lor_diag.
+
+Definition Nand_0_l : forall n, Nand 0 n = 0 := N.land_0_l.
+Definition Nand_0_r : forall n, Nand n 0 = 0 := N.land_0_r.
+Definition Nand_comm : forall a a', Nand a a' = Nand a' a := N.land_comm.
+Definition Nand_assoc :
+ forall a a' a'', Nand a (Nand a' a'') = Nand (Nand a a') a''
+ := N.land_assoc.
+Definition Nand_diag : forall a, Nand a a = a := N.land_diag.
+
+Definition Ndiff_0_l : forall n, Ndiff 0 n = 0 := N.ldiff_0_l.
+Definition Ndiff_0_r : forall n, Ndiff n 0 = n := N.ldiff_0_r.
+Definition Ndiff_diag : forall a, Ndiff a a = 0 := N.ldiff_diag.
+Definition Nor_and_distr_l : forall a b c,
+ Nor (Nand a b) c = Nand (Nor a c) (Nor b c)
+ := N.lor_land_distr_l.
+Definition Nor_and_distr_r : forall a b c,
+ Nor a (Nand b c) = Nand (Nor a b) (Nor a c)
+ := N.lor_land_distr_r.
+Definition Nand_or_distr_l : forall a b c,
+ Nand (Nor a b) c = Nor (Nand a c) (Nand b c)
+ := N.land_lor_distr_l.
+Definition Nand_or_distr_r : forall a b c,
+ Nand a (Nor b c) = Nor (Nand a b) (Nand a c)
+ := N.land_lor_distr_r.
+Definition Ndiff_diff_l : forall a b c,
+ Ndiff (Ndiff a b) c = Ndiff a (Nor b c)
+ := N.ldiff_ldiff_l.
+Definition Nor_diff_and : forall a b,
+ Nor (Ndiff a b) (Nand a b) = a
+ := N.lor_ldiff_and.
+Definition Nand_diff : forall a b,
+ Nand (Ndiff a b) b = 0
+ := N.land_ldiff.
 
 Local Close Scope N_scope.
 
 (** Checking whether a number is odd, i.e.
    if its lower bit is set. *)
 
-Definition Nbit0 (n:N) :=
-  match n with
-  | N0 => false
-  | Npos (_~0) => false
-  | _ => true
-  end.
+Notation Nbit0 := N.odd (only parsing).
 
 Definition Nodd (n:N) := Nbit0 n = true.
 Definition Neven (n:N) := Nbit0 n = false.
@@ -885,11 +580,7 @@ Qed.
 
 (** Number of digits in a number *)
 
-Definition Nsize (n:N) : nat := match n with
-  | N0 => O
-  | Npos p => Psize p
- end.
-
+Notation Nsize := N.size_nat (only parsing).
 
 (** conversions between N and bit vectors. *)
 
diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
index 0850a631e..559f01f16 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.v
@@ -6,155 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-Require Import BinPos BinNat.
-
+Require Import BinNat.
 Local Open Scope N_scope.
 
-Definition NPgeb (a:N)(b:positive) :=
-  match a with
-   | 0 => false
-   | Npos na => match Pos.compare na b with Lt => false | _ => true end
-  end.
-
-Local Notation "a >=? b" := (NPgeb a b) (at level 70).
-
-Fixpoint Pdiv_eucl (a b:positive) : N * N :=
-  match a with
-    | xH =>
-       match b with xH => (1, 0) | _ => (0, 1) end
-    | xO a' =>
-       let (q, r) := Pdiv_eucl a' b in
-       let r' := 2 * r in
-        if r' >=? b then (2 * q + 1, r' - Npos b)
-        else (2 * q, r')
-    | xI a' =>
-       let (q, r) := Pdiv_eucl a' b in
-       let r' := 2 * r + 1 in
-        if r' >=? b then (2 * q + 1, r' - Npos b)
-        else  (2 * q, r')
-  end.
-
-Definition Ndiv_eucl (a b:N) : N * N :=
-  match a, b with
-   | 0,  _ => (0, 0)
-   | _, 0  => (0, a)
-   | Npos na, Npos nb => Pdiv_eucl na nb
-  end.
-
-Definition Ndiv a b := fst (Ndiv_eucl a b).
-Definition Nmod a b := snd (Ndiv_eucl a b).
-
-Infix "/" := Ndiv : N_scope.
-Infix "mod" := Nmod (at level 40, no associativity) : N_scope.
-
-(** Auxiliary Results about [NPgeb] *)
+(** Obsolete file, see [BinNat] now,
+    only compatibility notations remain here. *)
 
-Lemma NPgeb_ge : forall a b, NPgeb a b = true -> a >= Npos b.
-Proof.
- destruct a; simpl; intros.
- discriminate.
- unfold Nge, Ncompare. now destruct Pos.compare.
-Qed.
+Definition Pdiv_eucl a b := N.pos_div_eucl a (Npos b).
 
-Lemma NPgeb_lt : forall a b, NPgeb a b = false -> a < Npos b.
-Proof.
- destruct a; simpl; intros. red; auto.
- unfold Nlt, Ncompare. now destruct Pos.compare.
-Qed.
+Definition Pdiv_eucl_correct a b :
+  let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + r
+ := N.pos_div_eucl_spec a (Npos b).
 
-Theorem NPgeb_correct: forall (a:N)(b:positive),
-  if NPgeb a b then a = a - Npos b + Npos b else True.
-Proof.
-  destruct a as [|a]; simpl; intros b; auto.
-  case Pos.compare_spec; intros; subst; auto.
-  now rewrite Pminus_mask_diag.
-  destruct (Pminus_mask_Gt a b (Pos.lt_gt _ _ H)) as [d [H2 [H3 _]]].
-  rewrite H2. rewrite <- H3.
-  simpl; f_equal; apply Pplus_comm.
-Qed.
-
-Lemma NPgeb_ineq0 : forall a p, a < Npos p -> NPgeb (2*a) p = true ->
- 2*a - Npos p < Npos p.
-Proof.
-intros a p LT GE.
-apply Nplus_lt_cancel_l with (Npos p).
-rewrite Nplus_comm.
-generalize (NPgeb_correct (2*a) p). rewrite GE. intros <-.
-rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r.
-destruct a; auto.
-Qed.
-
-Lemma NPgeb_ineq1 : forall a p, a < Npos p -> NPgeb (2*a+1) p = true ->
-  (2*a+1) - Npos p < Npos p.
-Proof.
-intros a p LT GE.
-apply Nplus_lt_cancel_l with (Npos p).
-rewrite Nplus_comm.
-generalize (NPgeb_correct (2*a+1) p). rewrite GE. intros <-.
-rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r.
-destruct a; auto.
-red; simpl. apply Pcompare_Gt_Lt; auto.
-Qed.
-
-(* Proofs of specifications for these euclidean divisions. *)
-
-Theorem Pdiv_eucl_correct: forall a b,
-  let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + r.
-Proof.
-  induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hq1.
-    assert (Npos a~1 = 2*q1*Npos b + (2*r1+1))
-     by now rewrite Nplus_assoc, <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1.
-    generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H'; auto.
-    rewrite Nmult_plus_distr_r, Nmult_1_l.
-    rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hq1.
-    assert (Npos a~0 = 2*q1*Npos b + 2*r1)
-     by now rewrite <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1.
-    generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H'; auto.
-    rewrite Nmult_plus_distr_r, Nmult_1_l.
-    rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto.
-  destruct b; auto.
-Qed.
-
-Theorem Ndiv_eucl_correct: forall a b,
-  let (q,r) := Ndiv_eucl a b in a = b * q + r.
-Proof.
-  destruct a as [|a]; destruct b as [|b]; simpl; auto.
-  generalize (Pdiv_eucl_correct a b); case Pdiv_eucl; intros q r.
-  destruct q. simpl; auto. rewrite Nmult_comm. intro EQ; exact EQ.
-Qed.
-
-Theorem Ndiv_mod_eq : forall a b,
-  a = b * (a/b) + (a mod b).
-Proof.
-  intros; generalize (Ndiv_eucl_correct a b).
-  unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl; auto.
-Qed.
-
-Theorem Pdiv_eucl_remainder : forall a b:positive,
+Lemma Pdiv_eucl_remainder a b :
   snd (Pdiv_eucl a b) < Npos b.
-Proof.
-  induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hr1; simpl in Hr1.
-    case_eq (NPgeb (2*r1+1) b); intros; unfold snd.
-    apply NPgeb_ineq1; auto.
-    apply NPgeb_lt; auto.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hr1; simpl in Hr1.
-    case_eq (NPgeb (2*r1) b); intros; unfold snd.
-    apply NPgeb_ineq0; auto.
-    apply NPgeb_lt; auto.
-  destruct b; simpl; reflexivity.
-Qed.
+Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed.
+
+Notation Ndiv_eucl := N.div_eucl (only parsing).
+Notation Ndiv := N.div (only parsing).
+Notation Nmod := N.modulo (only parsing).
 
-Theorem Nmod_lt : forall (a b:N), b<>0 -> a mod b < b.
-Proof.
-  destruct b as [ |b]; intro H; try solve [elim H;auto].
-  destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl.
-  generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; auto.
-Qed.
+Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing).
+Notation Ndiv_mod_eq := N.div_mod' (only parsing).
+Notation Nmod_lt := N.mod_lt (only parsing).
diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v
index c25af8717..13211f467 100644
--- a/theories/NArith/Ngcd_def.v
+++ b/theories/NArith/Ngcd_def.v
@@ -7,79 +7,16 @@
 (************************************************************************)
 
 Require Import BinPos BinNat.
-
 Local Open Scope N_scope.
 
-(** * Divisibility *)
-
-Definition Ndivide p q := exists r, p*r = q.
-Notation "( p | q )" := (Ndivide p q) (at level 0) : N_scope.
-
-(** * Definition of a Pgcd function for binary natural numbers *)
-
-Definition Ngcd (a b : N) :=
- match a, b with
-  | 0, _ => b
-  | _, 0 => a
-  | Npos p, Npos q => Npos (Pos.gcd p q)
- end.
-
-(** * Generalized Gcd, also computing rests of a and b after
-    division by gcd. *)
-
-Definition Nggcd (a b : N) :=
- match a, b with
-  | 0, _ => (b,(0,1))
-  | _, 0 => (a,(1,0))
-  | Npos p, Npos q =>
-     let '(g,(aa,bb)) := Pos.ggcd p q in
-     (Npos g, (Npos aa, Npos bb))
- end.
-
-(** The first component of Nggcd is Ngcd *)
-
-Lemma Nggcd_gcd : forall  a b, fst (Nggcd a b) = Ngcd a b.
-Proof.
- intros [ |p] [ |q]; simpl; auto.
- generalize (Pos.ggcd_gcd p q). destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence.
-Qed.
-
-(** The other components of Nggcd are indeed the correct factors. *)
-
-Lemma Nggcd_correct_divisors : forall a b,
-  let '(g,(aa,bb)) := Nggcd a b in
-  a=g*aa /\ b=g*bb.
-Proof.
- intros [ |p] [ |q]; simpl; auto.
- now rewrite Pmult_1_r.
- now rewrite Pmult_1_r.
- generalize (Pos.ggcd_correct_divisors p q).
- destruct Pos.ggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence.
-Qed.
-
-(** We can use this fact to prove a part of the gcd correctness *)
-
-Lemma Ngcd_divide_l : forall a b, (Ngcd a b | a).
-Proof.
- intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b).
- destruct Nggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto.
-Qed.
-
-Lemma Ngcd_divide_r : forall a b, (Ngcd a b | b).
-Proof.
- intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b).
- destruct Nggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto.
-Qed.
-
-(** We now prove directly that gcd is the greatest amongst common divisors *)
-
-Lemma Ngcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|Ngcd a b).
-Proof.
- intros [ |p] [ |q]; simpl; auto.
- intros [ |r]. intros (s,H). discriminate.
- intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *.
- 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.
-Qed.
+(** Obsolete file, see [BinNat] now,
+    only compatibility notations remain here. *)
+
+Notation Ndivide := N.divide (only parsing).
+Notation Ngcd := N.gcd (only parsing).
+Notation Nggcd := N.ggcd (only parsing).
+Notation Nggcd_gcd := N.ggcd_gcd (only parsing).
+Notation Nggcd_correct_divisors := N.ggcd_correct_divisors (only parsing).
+Notation Ngcd_divide_l := N.gcd_divide_l (only parsing).
+Notation Ngcd_divide_r := N.gcd_divide_r (only parsing).
+Notation Ngcd_greatest := N.gcd_greatest (only parsing).
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index 375ed0f90..edb6b2895 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -6,45 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Definition of a square root function for N. *)
+Require Import BinNat.
 
-Require Import BinPos BinNat.
+(** Obsolete file, see [BinNat] now,
+    only compatibility notations remain here. *)
 
-Local Open Scope N_scope.
-
-Definition Nsqrtrem n :=
- match n with
-  | N0 => (N0, N0)
-  | Npos p =>
-    match Pos.sqrtrem p with
-     | (s, IsPos r) => (Npos s, Npos r)
-     | (s, _) => (Npos s, N0)
-    end
- end.
-
-Definition Nsqrt n :=
- match n with
-  | N0 => N0
-  | Npos p => Npos (Pos.sqrt p)
- end.
-
-Lemma Nsqrtrem_spec : forall n,
- let (s,r) := Nsqrtrem n in n = s*s + r /\ r <= 2*s.
-Proof.
- destruct n. now split.
- generalize (Pos.sqrtrem_spec p). simpl.
- destruct 1; simpl; subst; now split.
-Qed.
-
-Lemma Nsqrt_spec : forall n,
- let s := Nsqrt n in s*s <= n < (Nsucc s)*(Nsucc s).
-Proof.
- destruct n. now split. apply (Pos.sqrt_spec p).
-Qed.
-
-Lemma Nsqrtrem_sqrt : forall n, fst (Nsqrtrem n) = Nsqrt n.
-Proof.
- destruct n. reflexivity.
- unfold Nsqrtrem, Nsqrt, Pos.sqrt.
- destruct (Pos.sqrtrem p) as (s,r). now destruct r.
-Qed.
\ No newline at end of file
+Notation Nsqrtrem := N.sqrtrem (only parsing).
+Notation Nsqrt := N.sqrt (only parsing).
+Notation Nsqrtrem_spec := N.sqrtrem_spec (only parsing).
+Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).
+Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (only parsing).