Move stuff about positive into a distinct PArith subdir

 Beware! after this, a ./configure must be done. It might also
 be a good idea to chase any phantom .vo remaining after a make clean

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

7 files changed, 1 insertions, 2035 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
deleted file mode 100644
index d334d42e9..000000000
--- a/theories/NArith/BinPos.v
+++ /dev/null
@@ -1,1260 +0,0 @@
-(* -*- coding: utf-8 -*- *)
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Unset Boxed Definitions.
-
-Declare ML Module "z_syntax_plugin".
-
-(**********************************************************************)
-(** Binary positive numbers *)
-
-(** Original development by Pierre Crégut, CNET, Lannion, France *)
-
-Inductive positive : Set :=
-| xI : positive -> positive
-| xO : positive -> positive
-| xH : positive.
-
-(** Declare binding key for scope positive_scope *)
-
-Delimit Scope positive_scope with positive.
-
-(** Automatically open scope positive_scope for type positive, xO and xI *)
-
-Bind Scope positive_scope with positive.
-Arguments Scope xO [positive_scope].
-Arguments Scope xI [positive_scope].
-
-(** Postfix notation for positive numbers, allowing to mimic
-    the position of bits in a big-endian representation.
-    For instance, we can write 1~1~0 instead of (xO (xI xH))
-    for the number 6 (which is 110 in binary notation).
-*)
-
-Notation "p ~ 1" := (xI p)
- (at level 7, left associativity, format "p '~' '1'") : positive_scope.
-Notation "p ~ 0" := (xO p)
- (at level 7, left associativity, format "p '~' '0'") : positive_scope.
-
-Open Local Scope positive_scope.
-
-(* In the current file, [xH] cannot yet be written as [1], since the
-   interpretation of positive numerical constants is not available
-   yet. We fix this here with an ad-hoc temporary notation. *)
-
-Notation Local "1" := xH (at level 7).
-
-(** Successor *)
-
-Fixpoint Psucc (x:positive) : positive :=
-  match x with
-    | p~1 => (Psucc p)~0
-    | p~0 => p~1
-    | 1 => 1~0
-  end.
-
-(** Addition *)
-
-Set Boxed Definitions.
-
-Fixpoint Pplus (x y:positive) : positive :=
-  match x, y with
-    | p~1, q~1 => (Pplus_carry p q)~0
-    | p~1, q~0 => (Pplus p q)~1
-    | p~1, 1 => (Psucc p)~0
-    | p~0, q~1 => (Pplus p q)~1
-    | p~0, q~0 => (Pplus p q)~0
-    | p~0, 1 => p~1
-    | 1, q~1 => (Psucc q)~0
-    | 1, q~0 => q~1
-    | 1, 1 => 1~0
-  end
-
-with Pplus_carry (x y:positive) : positive :=
-  match x, y with
-    | p~1, q~1 => (Pplus_carry p q)~1
-    | p~1, q~0 => (Pplus_carry p q)~0
-    | p~1, 1 => (Psucc p)~1
-    | p~0, q~1 => (Pplus_carry p q)~0
-    | p~0, q~0 => (Pplus p q)~1
-    | p~0, 1 => (Psucc p)~0
-    | 1, q~1 => (Psucc q)~1
-    | 1, q~0 => (Psucc q)~0
-    | 1, 1 => 1~1
-  end.
-
-Unset Boxed Definitions.
-
-Infix "+" := Pplus : positive_scope.
-
-Definition Piter_op {A}(op:A->A->A) :=
-  fix iter (p:positive)(a:A) : A :=
-  match p with
-    | 1 => a
-    | p~0 => iter p (op a a)
-    | p~1 => op a (iter p (op a a))
-  end.
-
-Lemma Piter_op_succ : forall A (op:A->A->A),
- (forall x y z, op x (op y z) = op (op x y) z) ->
- forall p a,
- Piter_op op (Psucc p) a = op a (Piter_op op p a).
-Proof.
- induction p; simpl; intros; trivial.
- rewrite H. apply IHp.
-Qed.
-
-(** From binary positive numbers to Peano natural numbers *)
-
-Definition Pmult_nat : positive -> nat -> nat :=
- Eval unfold Piter_op in (* for compatibility *)
- Piter_op plus.
-
-Definition nat_of_P (x:positive) := Pmult_nat x (S O).
-
-(** From Peano natural numbers to binary positive numbers *)
-
-Fixpoint P_of_succ_nat (n:nat) : positive :=
-  match n with
-    | O => 1
-    | S x => Psucc (P_of_succ_nat x)
-  end.
-
-(** Operation x -> 2*x-1 *)
-
-Fixpoint Pdouble_minus_one (x:positive) : positive :=
-  match x with
-    | p~1 => p~0~1
-    | p~0 => (Pdouble_minus_one p)~1
-    | 1 => 1
-  end.
-
-(** Predecessor *)
-
-Definition Ppred (x:positive) :=
-  match x with
-    | p~1 => p~0
-    | p~0 => Pdouble_minus_one p
-    | 1 => 1
-  end.
-
-(** An auxiliary type for subtraction *)
-
-Inductive positive_mask : Set :=
-| IsNul : positive_mask
-| IsPos : positive -> positive_mask
-| IsNeg : positive_mask.
-
-(** Operation x -> 2*x+1 *)
-
-Definition Pdouble_plus_one_mask (x:positive_mask) :=
-  match x with
-    | IsNul => IsPos 1
-    | IsNeg => IsNeg
-    | IsPos p => IsPos p~1
-  end.
-
-(** Operation x -> 2*x *)
-
-Definition Pdouble_mask (x:positive_mask) :=
-  match x with
-    | IsNul => IsNul
-    | IsNeg => IsNeg
-    | IsPos p => IsPos p~0
-  end.
-
-(** Operation x -> 2*x-2 *)
-
-Definition Pdouble_minus_two (x:positive) :=
-  match x with
-    | p~1 => IsPos p~0~0
-    | p~0 => IsPos (Pdouble_minus_one p)~0
-    | 1 => IsNul
-  end.
-
-(** Subtraction of binary positive numbers into a positive numbers mask *)
-
-Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask :=
-  match x, y with
-    | p~1, q~1 => Pdouble_mask (Pminus_mask p q)
-    | p~1, q~0 => Pdouble_plus_one_mask (Pminus_mask p q)
-    | p~1, 1 => IsPos p~0
-    | p~0, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
-    | p~0, q~0 => Pdouble_mask (Pminus_mask p q)
-    | p~0, 1 => IsPos (Pdouble_minus_one p)
-    | 1, 1 => IsNul
-    | 1, _ => IsNeg
-  end
-
-with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
-  match x, y with
-    | p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
-    | p~1, q~0 => Pdouble_mask (Pminus_mask p q)
-    | p~1, 1 => IsPos (Pdouble_minus_one p)
-    | p~0, q~1 => Pdouble_mask (Pminus_mask_carry p q)
-    | p~0, q~0 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
-    | p~0, 1 => Pdouble_minus_two p
-    | 1, _ => IsNeg
-  end.
-
-(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *)
-
-Definition Pminus (x y:positive) :=
-  match Pminus_mask x y with
-    | IsPos z => z
-    | _ => 1
-  end.
-
-Infix "-" := Pminus : positive_scope.
-
-(** Multiplication on binary positive numbers *)
-
-Fixpoint Pmult (x y:positive) : positive :=
-  match x with
-    | p~1 => y + (Pmult p y)~0
-    | p~0 => (Pmult p y)~0
-    | 1 => y
-  end.
-
-Infix "*" := Pmult : positive_scope.
-
-(** Division by 2 rounded below but for 1 *)
-
-Definition Pdiv2 (z:positive) :=
-  match z with
-    | 1 => 1
-    | p~0 => p
-    | p~1 => p
-  end.
-
-Infix "/" := Pdiv2 : positive_scope.
-
-(** Comparison on binary positive numbers *)
-
-Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
-  match x, y with
-    | p~1, q~1 => Pcompare p q r
-    | p~1, q~0 => Pcompare p q Gt
-    | p~1, 1 => Gt
-    | p~0, q~1 => Pcompare p q Lt
-    | p~0, q~0 => Pcompare p q r
-    | p~0, 1 => Gt
-    | 1, q~1 => Lt
-    | 1, q~0 => Lt
-    | 1, 1 => r
-  end.
-
-Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
-
-Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt.
-Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt.
-Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt.
-Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt.
-
-Infix "<=" := Ple : positive_scope.
-Infix "<" := Plt : positive_scope.
-Infix ">=" := Pge : positive_scope.
-Infix ">" := Pgt : positive_scope.
-
-Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
-Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
-Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
-Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
-
-
-Definition Pmin (p p' : positive) := match Pcompare p p' Eq with
- | Lt | Eq => p
- | Gt => p'
- end.
-
-Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
- | Lt | Eq => p'
- | Gt => p
- end.
-
-(********************************************************************)
-(** Boolean equality *)
-
-Fixpoint Peqb (x y : positive) {struct y} : bool :=
- match x, y with
- | 1, 1 => true
- | p~1, q~1 => Peqb p q
- | p~0, q~0 => Peqb p q
- | _, _ => false
- end.
-
-(**********************************************************************)
-(** Decidability of equality on binary positive numbers *)
-
-Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}.
-Proof.
-  decide equality.
-Defined.
-
-(* begin hide *)
-Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1.
-Proof.
-  intro; edestruct positive_eq_dec; eauto.
-Qed.
-(* end hide *)
-
-(**********************************************************************)
-(** Properties of successor on binary positive numbers *)
-
-(** Specification of [xI] in term of [Psucc] and [xO] *)
-
-Lemma xI_succ_xO : forall p:positive, p~1 = Psucc p~0.
-Proof.
-  reflexivity.
-Qed.
-
-Lemma Psucc_discr : forall p:positive, p <> Psucc p.
-Proof.
-  destruct p; discriminate.
-Qed.
-
-(** Successor and double *)
-
-Lemma Psucc_o_double_minus_one_eq_xO :
-  forall p:positive, Psucc (Pdouble_minus_one p) = p~0.
-Proof.
-  induction p; simpl; f_equal; auto.
-Qed.
-
-Lemma Pdouble_minus_one_o_succ_eq_xI :
-  forall p:positive, Pdouble_minus_one (Psucc p) = p~1.
-Proof.
-  induction p; simpl; f_equal; auto.
-Qed.
-
-Lemma xO_succ_permute :
-  forall p:positive, (Psucc p)~0 = Psucc (Psucc p~0).
-Proof.
-  induction p; simpl; auto.
-Qed.
-
-Lemma double_moins_un_xO_discr :
-  forall p:positive, Pdouble_minus_one p <> p~0.
-Proof.
-  destruct p; discriminate.
-Qed.
-
-(** Successor and predecessor *)
-
-Lemma Psucc_not_one : forall p:positive, Psucc p <> 1.
-Proof.
-  destruct p; discriminate.
-Qed.
-
-Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p.
-Proof.
-  intros [[p|p| ]|[p|p| ]| ]; simpl; auto.
-  f_equal; apply Pdouble_minus_one_o_succ_eq_xI.
-Qed.
-
-Lemma Psucc_pred : forall p:positive, p = 1 \/ Psucc (Ppred p) = p.
-Proof.
-  induction p; simpl; auto.
-  right; apply Psucc_o_double_minus_one_eq_xO.
-Qed.
-
-Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
-
-(** Injectivity of successor *)
-
-Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q.
-Proof.
-  induction p; intros [q|q| ] H; simpl in *; destr_eq H; f_equal; auto.
-  elim (Psucc_not_one p); auto.
-  elim (Psucc_not_one q); auto.
-Qed.
-
-(**********************************************************************)
-(** Properties of addition on binary positive numbers *)
-
-(** Specification of [Psucc] in term of [Pplus] *)
-
-Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + 1.
-Proof.
-  destruct p; reflexivity.
-Qed.
-
-Lemma Pplus_one_succ_l : forall p:positive, Psucc p = 1 + p.
-Proof.
-  destruct p; reflexivity.
-Qed.
-
-(** Specification of [Pplus_carry] *)
-
-Theorem Pplus_carry_spec :
-  forall p q:positive, Pplus_carry p q = Psucc (p + q).
-Proof.
-  induction p; destruct q; simpl; f_equal; auto.
-Qed.
-
-(** Commutativity *)
-
-Theorem Pplus_comm : forall p q:positive, p + q = q + p.
-Proof.
-  induction p; destruct q; simpl; f_equal; auto.
-  rewrite 2 Pplus_carry_spec; f_equal; auto.
-Qed.
-
-(** Permutation of [Pplus] and [Psucc] *)
-
-Theorem Pplus_succ_permute_r :
-  forall p q:positive, p + Psucc q = Psucc (p + q).
-Proof.
-  induction p; destruct q; simpl; f_equal;
-   auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto.
-Qed.
-
-Theorem Pplus_succ_permute_l :
-  forall p q:positive, Psucc p + q = Psucc (p + q).
-Proof.
-  intros p q; rewrite Pplus_comm, (Pplus_comm p);
-    apply Pplus_succ_permute_r.
-Qed.
-
-Theorem Pplus_carry_pred_eq_plus :
-  forall p q:positive, q <> 1 -> Pplus_carry p (Ppred q) = p + q.
-Proof.
-  intros p q H; rewrite Pplus_carry_spec, <- Pplus_succ_permute_r; f_equal.
-  destruct (Psucc_pred q); [ elim H; assumption | assumption ].
-Qed.
-
-(** No neutral for addition on strictly positive numbers *)
-
-Lemma Pplus_no_neutral : forall p q:positive, q + p <> p.
-Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] H;
-   destr_eq H; apply (IHp q H).
-Qed.
-
-Lemma Pplus_carry_no_neutral :
-  forall p q:positive, Pplus_carry q p <> Psucc p.
-Proof.
-  intros p q H; elim (Pplus_no_neutral p q).
-  apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption.
-Qed.
-
-(** Simplification *)
-
-Lemma Pplus_carry_plus :
-  forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s.
-Proof.
-  intros p q r s H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec;
-    assumption.
-Qed.
-
-Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q.
-Proof.
-  intros p q r; revert p q; induction r.
-  intros [p|p| ] [q|q| ] H; simpl; destr_eq H;
-    f_equal; auto using Pplus_carry_plus;
-    contradict H; auto using Pplus_carry_no_neutral.
-  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto;
-    contradict H; auto using Pplus_no_neutral.
-  intros p q H; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption.
-Qed.
-
-Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r.
-Proof.
-  intros p q r H; apply Pplus_reg_r with (r:=p).
-  rewrite (Pplus_comm r), (Pplus_comm q); assumption.
-Qed.
-
-Lemma Pplus_carry_reg_r :
-  forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q.
-Proof.
-  intros p q r H; apply Pplus_reg_r with (r:=r); apply Pplus_carry_plus;
-    assumption.
-Qed.
-
-Lemma Pplus_carry_reg_l :
-  forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r.
-Proof.
-  intros p q r H; apply Pplus_reg_r with (r:=p);
-  rewrite (Pplus_comm r), (Pplus_comm q); apply Pplus_carry_plus; assumption.
-Qed.
-
-(** Addition on positive is associative *)
-
-Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r.
-Proof.
-  induction p.
-  intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
-    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
-     ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
-  intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
-    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
-     ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
-  intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto.
-Qed.
-
-(** Commutation of addition with the double of a positive number *)
-
-Lemma Pplus_xO : forall m n : positive, (m + n)~0 = m~0 + n~0.
-Proof.
-  destruct n; destruct m; simpl; auto.
-Qed.
-
-Lemma Pplus_xI_double_minus_one :
-  forall p q:positive, (p + q)~0 = p~1 + Pdouble_minus_one q.
-Proof.
-  intros; change (p~1) with (p~0 + 1).
-  rewrite <- Pplus_assoc, <- Pplus_one_succ_l, Psucc_o_double_minus_one_eq_xO.
-  reflexivity.
-Qed.
-
-Lemma Pplus_xO_double_minus_one :
-  forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q.
-Proof.
-  induction p as [p IHp| p IHp| ]; destruct q; simpl;
-  rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI,
-    ?Pplus_xI_double_minus_one; try reflexivity.
-  rewrite IHp; auto.
-  rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity.
-Qed.
-
-(** Misc *)
-
-Lemma Pplus_diag : forall p:positive, p + p = p~0.
-Proof.
-  induction p as [p IHp| p IHp| ]; simpl;
-   try rewrite ?Pplus_carry_spec, ?IHp; reflexivity.
-Qed.
-
-(**********************************************************************)
-(** Peano induction and recursion on binary positive positive numbers *)
-(** (a nice proof from Conor McBride, see "The view from the left")   *)
-
-Inductive PeanoView : positive -> Type :=
-| PeanoOne : PeanoView 1
-| PeanoSucc : forall p, PeanoView p -> PeanoView (Psucc p).
-
-Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) :=
-  match q in PeanoView x return PeanoView (x~0) with
-    | PeanoOne => PeanoSucc _ PeanoOne
-    | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q))
-  end.
-
-Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) :=
-  match q in PeanoView x return PeanoView (x~1) with
-    | PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne)
-    | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q))
-  end.
-
-Fixpoint peanoView p : PeanoView p :=
-  match p return PeanoView p with
-    | 1 => PeanoOne
-    | p~0 => peanoView_xO p (peanoView p)
-    | p~1 => peanoView_xI p (peanoView p)
-  end.
-
-Definition PeanoView_iter (P:positive->Type)
-  (a:P 1) (f:forall p, P p -> P (Psucc p)) :=
-  (fix iter p (q:PeanoView p) : P p :=
-    match q in PeanoView p return P p with
-      | PeanoOne => a
-      | PeanoSucc _ q => f _ (iter _ q)
-    end).
-
-Require Import Eqdep_dec EqdepFacts.
-
-Theorem eq_dep_eq_positive :
-  forall (P:positive->Type) (p:positive) (x y:P p),
-    eq_dep positive P p x p y -> x = y.
-Proof.
-  apply eq_dep_eq_dec.
-  decide equality.
-Qed.
-
-Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.
-Proof.
-  intros.
-  induction q as [ | p q IHq ].
-  apply eq_dep_eq_positive.
-  cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial.
-  destruct p0; intros; discriminate.
-  trivial.
-  apply eq_dep_eq_positive.
-  cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'.
-  intro. destruct p; discriminate.
-  intro. unfold p0 in H. apply Psucc_inj in H.
-  generalize q'. rewrite H. intro.
-  rewrite (IHq q'0).
-  trivial.
-  trivial.
-Qed.
-
-Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p))
-  (p:positive) :=
-  PeanoView_iter P a f p (peanoView p).
-
-Theorem Prect_succ : forall (P:positive->Type) (a:P 1)
-  (f:forall p, P p -> P (Psucc p)) (p:positive),
-  Prect P a f (Psucc p) = f _ (Prect P a f p).
-Proof.
-  intros.
-  unfold Prect.
-  rewrite (PeanoViewUnique _ (peanoView (Psucc p)) (PeanoSucc _ (peanoView p))).
-  trivial.
-Qed.
-
-Theorem Prect_base : forall (P:positive->Type) (a:P 1)
-  (f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a.
-Proof.
-  trivial.
-Qed.
-
-Definition Prec (P:positive->Set) := Prect P.
-
-(** Peano induction *)
-
-Definition Pind (P:positive->Prop) := Prect P.
-
-(** Peano case analysis *)
-
-Theorem Pcase :
-  forall P:positive -> Prop,
-    P 1 -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p.
-Proof.
-  intros; apply Pind; auto.
-Qed.
-
-(**********************************************************************)
-(** Properties of multiplication on binary positive numbers *)
-
-(** One is right neutral for multiplication *)
-
-Lemma Pmult_1_r : forall p:positive, p * 1 = p.
-Proof.
-  induction p; simpl; f_equal; auto.
-Qed.
-
-(** Successor and multiplication *)
-
-Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m.
-Proof.
-  induction n as [n IHn | n IHn | ]; simpl; intro m.
-  rewrite IHn, Pplus_assoc, Pplus_diag, <-Pplus_xO; reflexivity.
-  reflexivity.
-  symmetry; apply Pplus_diag.
-Qed.
-
-(** Right reduction properties for multiplication *)
-
-Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0.
-Proof.
-  intros p q; induction p; simpl; do 2 (f_equal; auto).
-Qed.
-
-Lemma Pmult_xI_permute_r : forall p q:positive, p * q~1 = p + (p * q)~0.
-Proof.
-  intros p q; induction p as [p IHp|p IHp| ]; simpl; f_equal; auto.
-  rewrite IHp, 2 Pplus_assoc, (Pplus_comm p); reflexivity.
-Qed.
-
-(** Commutativity of multiplication *)
-
-Theorem Pmult_comm : forall p q:positive, p * q = q * p.
-Proof.
-  intros p q; induction q as [q IHq|q IHq| ]; simpl; try rewrite <- IHq;
-   auto using Pmult_xI_permute_r, Pmult_xO_permute_r, Pmult_1_r.
-Qed.
-
-(** Distributivity of multiplication over addition *)
-
-Theorem Pmult_plus_distr_l :
-  forall p q r:positive, p * (q + r) = p * q + p * r.
-Proof.
-  intros p q r; induction p as [p IHp|p IHp| ]; simpl.
-  rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0).
-  change ((p*q+p*r)~0) with (m+n).
-  rewrite 2 Pplus_assoc; f_equal.
-  rewrite <- 2 Pplus_assoc; f_equal.
-  apply Pplus_comm.
-  f_equal; auto.
-  reflexivity.
-Qed.
-
-Theorem Pmult_plus_distr_r :
-  forall p q r:positive, (p + q) * r = p * r + q * r.
-Proof.
-  intros p q r; do 3 rewrite Pmult_comm with (q:=r); apply Pmult_plus_distr_l.
-Qed.
-
-(** Associativity of multiplication *)
-
-Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r.
-Proof.
-  induction p as [p IHp| p IHp | ]; simpl; intros q r.
-  rewrite IHp; rewrite Pmult_plus_distr_r; reflexivity.
-  rewrite IHp; reflexivity.
-  reflexivity.
-Qed.
-
-(** Parity properties of multiplication *)
-
-Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r.
-Proof.
-  intros p q r; induction r; try discriminate.
-  rewrite 2 Pmult_xO_permute_r; intro H; destr_eq H; auto.
-Qed.
-
-Lemma Pmult_xO_discr : forall p q:positive, p~0 * q <> q.
-Proof.
-  intros p q; induction q; try discriminate.
-  rewrite Pmult_xO_permute_r; injection; assumption.
-Qed.
-
-(** Simplification properties of multiplication *)
-
-Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q.
-Proof.
-  induction p as [p IHp| p IHp| ]; intros [q|q| ] r H;
-    reflexivity || apply (f_equal (A:=positive)) || apply False_ind.
-  apply IHp with (r~0); simpl in *;
-    rewrite 2 Pmult_xO_permute_r; apply Pplus_reg_l with (1:=H).
-  apply Pmult_xI_mult_xO_discr with (1:=H).
-  simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1:=H).
-  symmetry in H; apply Pmult_xI_mult_xO_discr with (1:=H).
-  apply IHp with (r~0); simpl; rewrite 2 Pmult_xO_permute_r; assumption.
-  apply Pmult_xO_discr with (1:= H).
-  simpl in H; symmetry in H; rewrite Pplus_comm in H;
-    apply Pplus_no_neutral with (1:=H).
-  symmetry in H; apply Pmult_xO_discr with (1:=H).
-Qed.
-
-Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q.
-Proof.
-  intros p q r H; apply Pmult_reg_r with (r:=r).
-  rewrite (Pmult_comm p), (Pmult_comm q); assumption.
-Qed.
-
-(** Inversion of multiplication *)
-
-Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1.
-Proof.
-  intros [p|p| ] [q|q| ] H; destr_eq H; auto.
-Qed.
-
-(** Square *)
-
-Lemma Psquare_xO : forall p, p~0 * p~0 = (p*p)~0~0.
-Proof.
- intros. simpl. now rewrite Pmult_comm.
-Qed.
-
-Lemma Psquare_xI : forall p, p~1 * p~1 = (p*p+p)~0~1.
-Proof.
- intros. simpl. rewrite Pmult_comm. simpl. f_equal.
- rewrite Pplus_assoc, Pplus_diag. simpl. now rewrite Pplus_comm.
-Qed.
-
-(*********************************************************************)
-(** Properties of boolean equality *)
-
-Theorem Peqb_refl : forall x:positive, Peqb x x = true.
-Proof.
- induction x; auto.
-Qed.
-
-Theorem Peqb_true_eq : forall x y:positive, Peqb x y = true -> x=y.
-Proof.
- induction x; destruct y; simpl; intros; try discriminate.
- f_equal; auto.
- f_equal; auto.
- reflexivity.
-Qed.
-
-Theorem Peqb_eq : forall x y : positive, Peqb x y = true <-> x=y.
-Proof.
- split. apply Peqb_true_eq.
- intros; subst; apply Peqb_refl.
-Qed.
-
-
-(**********************************************************************)
-(** Properties of comparison on binary positive numbers *)
-
-Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq.
-  induction p; auto.
-Qed.
-
-(* A generalization of Pcompare_refl *)
-
-Theorem Pcompare_refl_id : forall (p : positive) (r : comparison), (p ?= p) r = r.
-  induction p; auto.
-Qed.
-
-Theorem Pcompare_not_Eq :
-  forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq.
-Proof.
-  induction p as [p IHp| p IHp| ]; intros [q| q| ]; split; simpl; auto;
-    discriminate || (elim (IHp q); auto).
-Qed.
-
-Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
-Proof.
-  induction p; intros [q| q| ] H; simpl in *; auto;
-   try discriminate H; try (f_equal; auto; fail).
-  destruct (Pcompare_not_Eq p q) as (H',_); elim H'; auto.
-  destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto.
-Qed.
-
-Lemma Pcompare_eq_iff : forall p q:positive, (p ?= q) Eq = Eq <-> p = q.
-Proof.
-  split.
-  apply Pcompare_Eq_eq.
-  intros; subst; apply Pcompare_refl.
-Qed.
-
-Lemma Pcompare_Gt_Lt :
-  forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt.
-Proof.
-  induction p; intros [q|q| ] H; simpl; auto; discriminate.
-Qed.
-
-Lemma Pcompare_eq_Lt :
-  forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt.
-Proof.
-  intros p q; split; [| apply Pcompare_Gt_Lt].
-  revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate.
-Qed.
-
-Lemma Pcompare_Lt_Gt :
-  forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt.
-Proof.
-  induction p; intros [q|q| ] H; simpl; auto; discriminate.
-Qed.
-
-Lemma Pcompare_eq_Gt :
-  forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt.
-Proof.
-  intros p q; split; [| apply Pcompare_Lt_Gt].
-  revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate.
-Qed.
-
-Lemma Pcompare_Lt_Lt :
-  forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q.
-Proof.
-  induction p as [p IHp| p IHp| ]; intros [q|q| ] H; simpl in *; auto;
-   destruct (IHp q H); subst; auto.
-Qed.
-
-Lemma Pcompare_Lt_eq_Lt :
-  forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q.
-Proof.
-  intros p q; split; [apply Pcompare_Lt_Lt |].
-  intros [H|H]; [|subst; apply Pcompare_refl_id].
-  revert q H; induction p; intros [q|q| ] H; simpl in *;
-  auto; discriminate.
-Qed.
-
-Lemma Pcompare_Gt_Gt :
-  forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q.
-Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto;
-    destruct (IHp q H); subst; auto.
-Qed.
-
-Lemma Pcompare_Gt_eq_Gt :
-  forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q.
-Proof.
-  intros p q; split; [apply Pcompare_Gt_Gt |].
-  intros [H|H]; [|subst; apply Pcompare_refl_id].
-  revert q H; induction p; intros [q|q| ] H; simpl in *;
-  auto; discriminate.
-Qed.
-
-Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.
-Proof.
-  destruct r; auto.
-Qed.
-
-Ltac ElimPcompare c1 c2 :=
-  elim (Dcompare ((c1 ?= c2) Eq));
-    [ idtac | let x := fresh "H" in (intro x; case x; clear x) ].
-
-Lemma Pcompare_antisym :
-  forall (p q:positive) (r:comparison),
-    CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).
-Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto;
-   rewrite IHp; auto.
-Qed.
-
-Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt.
-Proof.
-  intros p q H; change Eq with (CompOpp Eq).
-  rewrite <- Pcompare_antisym, H; reflexivity.
-Qed.
-
-Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt.
-Proof.
-  intros p q H; change Eq with (CompOpp Eq).
-  rewrite <- Pcompare_antisym, H; reflexivity.
-Qed.
-
-Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq.
-Proof.
-  intros p q H; change Eq with (CompOpp Eq).
-  rewrite <- Pcompare_antisym, H; reflexivity.
-Qed.
-
-Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq).
-Proof.
-  intros; change Eq at 1 with (CompOpp Eq).
-  symmetry; apply Pcompare_antisym.
-Qed.
-
-Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq).
-Proof.
-  intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor.
-  apply Pcompare_Eq_eq; auto.
-  auto.
-  apply ZC1; auto.
-Qed.
-
-
-(** Comparison and the successor *)
-
-Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
-Proof.
-  induction p; simpl in *;
-    [ elim (Pcompare_eq_Lt p (Psucc p)); auto |
-      apply Pcompare_refl_id | reflexivity].
-Qed.
-
-Theorem Pcompare_p_Sq : forall p q : positive,
-  (p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q.
-Proof.
-  intros p q; split.
-  (* -> *)
-  revert p q; induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *;
-   try (left; reflexivity); try (right; reflexivity).
-  destruct (IHp q (Pcompare_Gt_Lt _ _ H)); subst; auto.
-  destruct (Pcompare_eq_Lt p q); auto.
-  destruct p; discriminate.
-  left; destruct (IHp q H);
-   [ elim (Pcompare_Lt_eq_Lt p q); auto | subst; apply Pcompare_refl_id].
-  destruct (Pcompare_Lt_Lt p q H); subst; auto.
-  destruct p; discriminate.
-  (* <- *)
-  intros [H|H]; [|subst; apply Pcompare_p_Sp].
-  revert q H; induction p; intros [q|q| ] H; simpl in *;
-   auto; try discriminate.
-  destruct (Pcompare_eq_Lt p (Psucc q)); auto.
-  apply Pcompare_Gt_Lt; auto.
-  destruct (Pcompare_Lt_Lt p q H); subst; auto using Pcompare_p_Sp.
-  destruct (Pcompare_Lt_eq_Lt p q); auto.
-Qed.
-
-(** 1 is the least positive number *)
-
-Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt.
-Proof.
-  destruct p; discriminate.
-Qed.
-
-(** Properties of the strict order on positive numbers *)
-
-Lemma Plt_1 : forall p, ~ p < 1.
-Proof.
- exact Pcompare_1.
-Qed.
-
-Lemma Plt_1_succ : forall n, 1 < Psucc n.
-Proof.
- intros. apply Pcompare_p_Sq. destruct n; auto.
-Qed.
-
-Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m.
-Proof.
-  unfold Plt; intros n m H; apply <- Pcompare_p_Sq; auto.
-Qed.
-
-Lemma Psucc_lt_compat : forall n m, n < m <-> Psucc n < Psucc m.
-Proof.
- unfold Plt. induction n; destruct m; simpl; auto; split; try easy; intros.
- now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, IHn, Pcompare_Gt_Lt.
- now apply Pcompare_eq_Lt, IHn, Pcompare_p_Sq, Pcompare_Lt_eq_Lt.
- destruct (Psucc n); discriminate.
- now apply Pcompare_eq_Lt, Pcompare_p_Sq, Pcompare_Lt_eq_Lt.
- now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, Pcompare_Gt_Lt.
- destruct n; discriminate.
- apply Plt_1_succ.
- destruct m; auto.
-Qed.
-
-Lemma Plt_irrefl : forall p : positive, ~ p < p.
-Proof.
-  unfold Plt; intro p; rewrite Pcompare_refl; discriminate.
-Qed.
-
-Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p.
-Proof.
-  intros n m p; induction p using Pind; intros H H0.
-  elim (Plt_1 _ H0).
-  apply Plt_lt_succ.
-  destruct (Pcompare_p_Sq m p) as (H',_); destruct (H' H0); subst; auto.
-Qed.
-
-Theorem Plt_ind : forall (A : positive -> Prop) (n : positive),
-  A (Psucc n) ->
-    (forall m : positive, n < m -> A m -> A (Psucc m)) ->
-      forall m : positive, n < m -> A m.
-Proof.
-  intros A n AB AS m. induction m using Pind; intros H.
-  elim (Plt_1 _ H).
-  destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto.
-Qed.
-
-Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q.
-Proof.
-  unfold Ple, Plt. intros.
-  generalize (Pcompare_eq_iff p q).
-  destruct ((p ?= q) Eq); intuition; discriminate.
-Qed.
-
-(** Strict order and operations *)
-
-Lemma Pplus_lt_mono_l : forall p q r, q<r <-> p+q < p+r.
-Proof.
- induction p using Prect.
- intros q r. rewrite <- 2 Pplus_one_succ_l. apply Psucc_lt_compat.
- intros q r. rewrite 2 Pplus_succ_permute_l.
- eapply iff_trans; [ eapply IHp | eapply Psucc_lt_compat ].
-Qed.
-
-Lemma Pplus_lt_mono : forall p q r s, p<q -> r<s -> p+r<q+s.
-Proof.
- intros. apply Plt_trans with (p+s).
- now apply Pplus_lt_mono_l.
- rewrite (Pplus_comm p), (Pplus_comm q). now apply Pplus_lt_mono_l.
-Qed.
-
-Lemma Pmult_lt_mono_l : forall p q r, q<r -> p*q < p*r.
-Proof.
- induction p using Prect; auto.
- intros q r H. rewrite 2 Pmult_Sn_m.
- apply Pplus_lt_mono; auto.
-Qed.
-
-Lemma Pmult_lt_mono : forall p q r s, p<q -> r<s -> p*r < q*s.
-Proof.
- intros. apply Plt_trans with (p*s).
- now apply Pmult_lt_mono_l.
- rewrite (Pmult_comm p), (Pmult_comm q). now apply Pmult_lt_mono_l.
-Qed.
-
-Lemma Plt_plus_r : forall p q, p < p+q.
-Proof.
- induction q using Prect.
- rewrite <- Pplus_one_succ_r. apply Pcompare_p_Sp.
- apply Plt_trans with (p+q); auto.
- apply Pplus_lt_mono_l, Pcompare_p_Sp.
-Qed.
-
-Lemma Plt_not_plus_l : forall p q, ~ p+q < p.
-Proof.
- intros p q H. elim (Plt_irrefl p).
- apply Plt_trans with (p+q); auto using Plt_plus_r.
-Qed.
-
-
-(**********************************************************************)
-(** Properties of subtraction on binary positive numbers *)
-
-Lemma Ppred_minus : forall p, Ppred p = Pminus p 1.
-Proof.
-  destruct p; auto.
-Qed.
-
-Definition Ppred_mask (p : positive_mask) :=
-match p with
-| IsPos 1 => IsNul
-| IsPos q => IsPos (Ppred q)
-| IsNul => IsNeg
-| IsNeg => IsNeg
-end.
-
-Lemma Pminus_mask_succ_r :
-  forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q.
-Proof.
-  induction p ; destruct q; simpl; f_equal; auto; destruct p; auto.
-Qed.
-
-Theorem Pminus_mask_carry_spec :
-  forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q).
-Proof.
-  induction p as [p IHp|p IHp| ]; destruct q; simpl;
-   try reflexivity; try rewrite IHp;
-   destruct (Pminus_mask p q) as [|[r|r| ]|] || destruct p; auto.
-Qed.
-
-Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q).
-Proof.
-  intros p q; unfold Pminus;
-  rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
-  destruct (Pminus_mask p q) as [|[r|r| ]|]; auto.
-Qed.
-
-Lemma double_eq_zero_inversion :
-  forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul.
-Proof.
-  destruct p; simpl; intros; trivial; discriminate.
-Qed.
-
-Lemma double_plus_one_zero_discr :
-  forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul.
-Proof.
-  destruct p; discriminate.
-Qed.
-
-Lemma double_plus_one_eq_one_inversion :
-  forall p:positive_mask, Pdouble_plus_one_mask p = IsPos 1 -> p = IsNul.
-Proof.
-  destruct p; simpl; intros; trivial; discriminate.
-Qed.
-
-Lemma double_eq_one_discr :
-  forall p:positive_mask, Pdouble_mask p <> IsPos 1.
-Proof.
-  destruct p; discriminate.
-Qed.
-
-Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul.
-Proof.
-  induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
-Qed.
-
-Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg.
-Proof.
-  induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
-Qed.
-
-Lemma Pminus_mask_IsNeg : forall p q:positive,
- Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
-Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto;
-   try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H;
-   specialize IHp with q.
-  destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
-  destruct (Pminus_mask p q); simpl; auto; try discriminate.
-  destruct (Pminus_mask_carry p q); simpl; auto; try discriminate.
-  destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
-Qed.
-
-Lemma ZL10 :
-  forall p q:positive,
-    Pminus_mask p q = IsPos 1 -> Pminus_mask_carry p q = IsNul.
-Proof.
-  induction p; intros [q|q| ] H; simpl in *; try discriminate.
-  elim (double_eq_one_discr _ H).
-  rewrite (double_plus_one_eq_one_inversion _ H); auto.
-  rewrite (double_plus_one_eq_one_inversion _ H); auto.
-  elim (double_eq_one_discr _ H).
-  destruct p; simpl; auto; discriminate.
-Qed.
-
-(** Properties of subtraction valid only for x>y *)
-
-Lemma Pminus_mask_Gt :
-  forall p q:positive,
-    (p ?= q) Eq = Gt ->
-    exists h : positive,
-      Pminus_mask p q = IsPos h /\
-      q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).
-Proof.
-  induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *;
-   try discriminate H.
-  (* p~1, q~1 *)
-  destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
-  repeat split; auto; right.
-  destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
-  rewrite ZL10; subst; auto.
-  rewrite W; simpl; destruct r; auto; elim NE; auto.
-  (* p~1, q~0 *)
-  destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H.
-  destruct (IHp q H) as (r & U & V & W); exists (r~1); rewrite ?U, ?V; auto.
-  exists 1; subst; rewrite Pminus_mask_diag; auto.
-  (* p~1, 1 *)
-  exists (p~0); auto.
-  (* p~0, q~1 *)
-  destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as (r & U & V & W).
-  destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
-  exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto.
-  exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto.
-  (* p~0, q~0 *)
-  destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
-  repeat split; auto; right.
-  destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
-  rewrite ZL10; subst; auto.
-  rewrite W; simpl; destruct r; auto; elim NE; auto.
-  (* p~0, 1 *)
-  exists (Pdouble_minus_one p); repeat split; destruct p; simpl; auto.
-  rewrite Psucc_o_double_minus_one_eq_xO; auto.
-Qed.
-
-Theorem Pplus_minus :
-  forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p.
-Proof.
-  intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _).
-  unfold Pminus; rewrite U; simpl; auto.
-Qed.
-
-(** When x<y, the substraction of x by y returns 1 *)
-
-Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg.
-Proof.
-  unfold Plt; induction p as [p IHp|p IHp| ]; destruct q; simpl; intros;
-   try discriminate; try rewrite IHp; auto.
-  apply Pcompare_Gt_Lt; auto.
-  destruct (Pcompare_Lt_Lt _ _ H).
-  rewrite Pminus_mask_IsNeg; simpl; auto.
-  subst; rewrite Pminus_mask_carry_diag; auto.
-Qed.
-
-Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = 1.
-Proof.
-  intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto.
-Qed.
-
-(** The substraction of x by x returns 1 *)
-
-Lemma Pminus_Eq : forall p:positive, p-p = 1.
-Proof.
- intros; unfold Pminus; rewrite Pminus_mask_diag; auto.
-Qed.
-
-(** Number of digits in a number *)
-
-Fixpoint Psize (p:positive) : nat :=
-  match p with
-    | 1 => S O
-    | p~1 => S (Psize p)
-    | p~0 => S (Psize p)
-  end.
-
-Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat.
-Proof.
-  assert (le0 : forall n, (0<=n)%nat) by (induction n; auto).
-  assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto).
-  induction p; destruct q; simpl; auto; intros; try discriminate.
-  intros; generalize (Pcompare_Gt_Lt _ _ H); auto.
-  intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto.
-Qed.
-
-
-
-
-
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
deleted file mode 100644
index 1c4cde6f5..000000000
--- a/theories/NArith/POrderedType.v
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import BinPos Equalities Orders OrdersTac.
-
-Local Open Scope positive_scope.
-
-(** * DecidableType structure for [positive] numbers *)
-
-Module Positive_as_UBE <: UsualBoolEq.
- Definition t := positive.
- Definition eq := @eq positive.
- Definition eqb := Peqb.
- Definition eqb_eq := Peqb_eq.
-End Positive_as_UBE.
-
-Module Positive_as_DT <: UsualDecidableTypeFull
- := Make_UDTF Positive_as_UBE.
-
-(** Note that the last module fulfills by subtyping many other
-    interfaces, such as [DecidableType] or [EqualityType]. *)
-
-
-
-(** * OrderedType structure for [positive] numbers *)
-
-Module Positive_as_OT <: OrderedTypeFull.
- Include Positive_as_DT.
- Definition lt := Plt.
- Definition le := Ple.
- Definition compare p q := Pcompare p q Eq.
-
- Instance lt_strorder : StrictOrder Plt.
- Proof. split; [ exact Plt_irrefl | exact Plt_trans ]. Qed.
-
- Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Plt.
- Proof. repeat red; intros; subst; auto. Qed.
-
- Definition le_lteq := Ple_lteq.
- Definition compare_spec := Pcompare_spec.
-
-End Positive_as_OT.
-
-(** Note that [Positive_as_OT] can also be seen as a [UsualOrderedType]
-   and a [OrderedType] (and also as a [DecidableType]). *)
-
-
-
-(** * An [order] tactic for positive numbers *)
-
-Module PositiveOrder := OTF_to_OrderTac Positive_as_OT.
-Ltac p_order := PositiveOrder.order.
-
-(** Note that [p_order] is domain-agnostic: it will not prove
-    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v
deleted file mode 100644
index 2f753a4c9..000000000
--- a/theories/NArith/Pminmax.v
+++ /dev/null
@@ -1,126 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Orders BinPos Pnat POrderedType GenericMinMax.
-
-(** * Maximum and Minimum of two positive numbers *)
-
-Local Open Scope positive_scope.
-
-(** The functions [Pmax] and [Pmin] implement indeed
-    a maximum and a minimum *)
-
-Lemma Pmax_l : forall x y, y<=x -> Pmax x y = x.
-Proof.
- unfold Ple, Pmax. intros x y.
- rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y).
- destruct ((x ?= y) Eq); intuition.
-Qed.
-
-Lemma Pmax_r : forall x y, x<=y -> Pmax x y = y.
-Proof.
- unfold Ple, Pmax. intros x y. destruct ((x ?= y) Eq); intuition.
-Qed.
-
-Lemma Pmin_l : forall x y, x<=y -> Pmin x y = x.
-Proof.
- unfold Ple, Pmin. intros x y. destruct ((x ?= y) Eq); intuition.
-Qed.
-
-Lemma Pmin_r : forall x y, y<=x -> Pmin x y = y.
-Proof.
- unfold Ple, Pmin. intros x y.
- rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y).
- destruct ((x ?= y) Eq); intuition.
-Qed.
-
-Module PositiveHasMinMax <: HasMinMax Positive_as_OT.
- Definition max := Pmax.
- Definition min := Pmin.
- Definition max_l := Pmax_l.
- Definition max_r := Pmax_r.
- Definition min_l := Pmin_l.
- Definition min_r := Pmin_r.
-End PositiveHasMinMax.
-
-
-Module P.
-(** We obtain hence all the generic properties of max and min. *)
-
-Include UsualMinMaxProperties Positive_as_OT PositiveHasMinMax.
-
-(** * Properties specific to the [positive] domain *)
-
-(** Simplifications *)
-
-Lemma max_1_l : forall n, Pmax 1 n = n.
-Proof.
- intros. unfold Pmax. rewrite ZC4. generalize (Pcompare_1 n).
- destruct (n ?= 1); intuition.
-Qed.
-
-Lemma max_1_r : forall n, Pmax n 1 = n.
-Proof. intros. rewrite P.max_comm. apply max_1_l. Qed.
-
-Lemma min_1_l : forall n, Pmin 1 n = 1.
-Proof.
- intros. unfold Pmin. rewrite ZC4. generalize (Pcompare_1 n).
- destruct (n ?= 1); intuition.
-Qed.
-
-Lemma min_1_r : forall n, Pmin n 1 = 1.
-Proof. intros. rewrite P.min_comm. apply min_1_l. Qed.
-
-(** Compatibilities (consequences of monotonicity) *)
-
-Lemma succ_max_distr :
- forall n m, Psucc (Pmax n m) = Pmax (Psucc n) (Psucc m).
-Proof.
- intros. symmetry. apply max_monotone.
- intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism.
- simpl; auto.
-Qed.
-
-Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m).
-Proof.
- intros. symmetry. apply min_monotone.
- intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism.
- simpl; auto.
-Qed.
-
-Lemma plus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m.
-Proof.
- intros. apply max_monotone.
- intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism.
- rewrite <- 2 Compare_dec.nat_compare_le. auto with arith.
-Qed.
-
-Lemma plus_max_distr_r : forall n m p, Pmax (n + p) (m + p) = Pmax n m + p.
-Proof.
- intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p).
- apply plus_max_distr_l.
-Qed.
-
-Lemma plus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m.
-Proof.
- intros. apply min_monotone.
- intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism.
- rewrite <- 2 Compare_dec.nat_compare_le. auto with arith.
-Qed.
-
-Lemma plus_min_distr_r : forall n m p, Pmin (n + p) (m + p) = Pmin n m + p.
-Proof.
- intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p).
- apply plus_min_distr_l.
-Qed.
-
-End P.
\ No newline at end of file
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v
deleted file mode 100644
index 715c4484d..000000000
--- a/theories/NArith/Pnat.v
+++ /dev/null
@@ -1,460 +0,0 @@
-(* -*- coding: utf-8 -*- *)
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import BinPos.
-
-(**********************************************************************)
-(** Properties of the injection from binary positive numbers to Peano
-    natural numbers *)
-
-(** Original development by Pierre Crégut, CNET, Lannion, France *)
-
-Require Import Le.
-Require Import Lt.
-Require Import Gt.
-Require Import Plus.
-Require Import Mult.
-Require Import Minus.
-Require Import Compare_dec.
-
-Local Open Scope positive_scope.
-Local Open Scope nat_scope.
-
-(** [nat_of_P] is a morphism for addition *)
-
-Lemma Pmult_nat_succ_morphism :
- forall (p:positive) (n:nat), Pmult_nat (Psucc p) n = n + Pmult_nat p n.
-Proof.
-intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m;
- rewrite IHp; rewrite plus_assoc; trivial.
-Qed.
-
-Lemma nat_of_P_succ_morphism :
- forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p).
-Proof.
-  intro; change (S (nat_of_P p)) with (1 + nat_of_P p) in |- *;
-   unfold nat_of_P in |- *; apply Pmult_nat_succ_morphism.
-Qed.
-
-Theorem Pmult_nat_plus_carry_morphism :
- forall (p q:positive) (n:nat),
-   Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n.
-Proof.
-intro x; induction x as [p IHp| p IHp| ]; intro y;
- [ destruct y as [p0| p0| ]
- | destruct y as [p0| p0| ]
- | destruct y as [p| p| ] ]; simpl in |- *; auto with arith;
- intro m;
- [ rewrite IHp; rewrite plus_assoc; trivial with arith
- | rewrite IHp; rewrite plus_assoc; trivial with arith
- | rewrite Pmult_nat_succ_morphism; rewrite plus_assoc; trivial with arith
- | rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].
-Qed.
-
-Theorem nat_of_P_plus_carry_morphism :
- forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)).
-Proof.
-intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism;
- simpl in |- *; trivial with arith.
-Qed.
-
-Theorem Pmult_nat_l_plus_morphism :
- forall (p q:positive) (n:nat),
-   Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.
-Proof.
-intro x; induction x as [p IHp| p IHp| ]; intro y;
- [ destruct y as [p0| p0| ]
- | destruct y as [p0| p0| ]
- | destruct y as [p| p| ] ]; simpl in |- *; auto with arith;
- [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp;
-    rewrite plus_assoc_reverse; rewrite plus_assoc_reverse;
-    rewrite (plus_permute m (Pmult_nat p (m + m)));
-    trivial with arith
- | intros m; rewrite IHp; apply plus_assoc
- | intros m; rewrite Pmult_nat_succ_morphism;
-    rewrite (plus_comm (m + Pmult_nat p (m + m)));
-    apply plus_assoc_reverse
- | intros m; rewrite IHp; apply plus_permute
- | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].
-Qed.
-
-Theorem nat_of_P_plus_morphism :
- forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q.
-Proof.
-intros x y; exact (Pmult_nat_l_plus_morphism x y 1).
-Qed.
-
-(** [Pmult_nat] is a morphism for addition *)
-
-Lemma Pmult_nat_r_plus_morphism :
- forall (p:positive) (n:nat),
-   Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n.
-Proof.
-intro y; induction y as [p H| p H| ]; intro m;
- [ simpl in |- *; rewrite H; rewrite plus_assoc_reverse;
-    rewrite (plus_permute m (Pmult_nat p (m + m)));
-    rewrite plus_assoc_reverse; auto with arith
- | simpl in |- *; rewrite H; auto with arith
- | simpl in |- *; trivial with arith ].
-Qed.
-
-Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p.
-Proof.
-intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism;
- trivial.
-Qed.
-
-(** [nat_of_P] is a morphism for multiplication *)
-
-Theorem nat_of_P_mult_morphism :
- forall p q:positive, nat_of_P (p * q) = nat_of_P p * nat_of_P q.
-Proof.
-intros x y; induction x as [x' H| x' H| ];
- [ change (xI x' * y)%positive with (y + xO (x' * y))%positive in |- *;
-    rewrite nat_of_P_plus_morphism; unfold nat_of_P at 2 3 in |- *;
-    simpl in |- *; do 2 rewrite ZL6; rewrite H; rewrite mult_plus_distr_r;
-    reflexivity
- | unfold nat_of_P at 1 2 in |- *; simpl in |- *; do 2 rewrite ZL6; rewrite H;
-    rewrite mult_plus_distr_r; reflexivity
- | simpl in |- *; rewrite <- plus_n_O; reflexivity ].
-Qed.
-
-(** [nat_of_P] maps to the strictly positive subset of [nat] *)
-
-Lemma ZL4 : forall p:positive,  exists h : nat, nat_of_P p = S h.
-Proof.
-intro y; induction y as [p H| p H| ];
- [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *;
-    simpl in |- *; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1;
-    rewrite H1; auto with arith
- | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *;
-    simpl in |- *; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2;
-    rewrite H2; auto with arith
- | exists 0; auto with arith ].
-Qed.
-
-(** Extra lemmas on [lt] on Peano natural numbers *)
-
-Lemma ZL7 : forall n m:nat, n < m -> n + n < m + m.
-Proof.
-intros m n H; apply lt_trans with (m := m + n);
- [ apply plus_lt_compat_l with (1 := H)
- | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].
-Qed.
-
-Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m.
-Proof.
-intros m n H; apply le_lt_trans with (m := m + n);
- [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H)
- | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
-    from [compare] on [positive])
-
-    Part 1: [lt] on [positive] is finer than [lt] on [nat]
-*)
-
-Lemma nat_of_P_lt_Lt_compare_morphism :
- forall p q:positive, (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q.
-Proof.
-intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ];
- intro H2;
- [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6;
-    apply ZL7; apply H; simpl in H2; assumption
- | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8;
-    apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption
- | simpl in |- *; discriminate H2
- | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    elim (Pcompare_Lt_Lt p q H2);
-    [ intros H3; apply lt_S; apply ZL7; apply H; apply H3
-    | intros E; rewrite E; apply lt_n_Sn ]
- | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    apply ZL7; apply H; assumption
- | simpl in |- *; discriminate H2
- | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6;
-    elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *;
-    apply lt_O_Sn
- | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q);
-    intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;
-    apply lt_n_S; apply lt_O_Sn
- | simpl in |- *; discriminate H2 ].
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
-    from [compare] on [positive])
-
-    Part 1: [gt] on [positive] is finer than [gt] on [nat]
-*)
-
-Lemma nat_of_P_gt_Gt_compare_morphism :
- forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q.
-Proof.
-intros p q GT. unfold gt.
-apply nat_of_P_lt_Lt_compare_morphism.
-change ((q ?= p) (CompOpp Eq) = CompOpp Gt).
-rewrite <- Pcompare_antisym, GT; auto.
-Qed.
-
-(** [nat_of_P] is a morphism for [Pcompare] and [nat_compare] *)
-
-Lemma nat_of_P_compare_morphism : forall p q,
- (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q).
-Proof.
- intros p q; symmetry.
- destruct ((p ?= q) Eq) as [ | | ]_eqn.
- rewrite (Pcompare_Eq_eq p q); auto.
- apply <- nat_compare_eq_iff; auto.
- apply -> nat_compare_lt. apply nat_of_P_lt_Lt_compare_morphism; auto.
- apply -> nat_compare_gt. apply nat_of_P_gt_Gt_compare_morphism; auto.
-Qed.
-
-(** [nat_of_P] is hence injective. *)
-
-Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q.
-Proof.
-intros.
-apply Pcompare_Eq_eq.
-rewrite nat_of_P_compare_morphism.
-apply <- nat_compare_eq_iff; auto.
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
-    from [compare] on [positive])
-
-    Part 2: [lt] on [nat] is finer than [lt] on [positive]
-*)
-
-Lemma nat_of_P_lt_Lt_compare_complement_morphism :
- forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt.
-Proof.
- intros. rewrite nat_of_P_compare_morphism.
- apply -> nat_compare_lt; auto.
-Qed.
-
-(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
-    from [compare] on [positive])
-
-    Part 2: [gt] on [nat] is finer than [gt] on [positive]
-*)
-
-Lemma nat_of_P_gt_Gt_compare_complement_morphism :
- forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt.
-Proof.
- intros. rewrite nat_of_P_compare_morphism.
- apply -> nat_compare_gt; auto.
-Qed.
-
-
-(** [nat_of_P] is strictly positive *)
-
-Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n.
-induction p; simpl in |- *; auto with arith.
-intro m; apply le_trans with (m + m); auto with arith.
-Qed.
-
-Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p.
-intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith.
-apply le_Pmult_nat.
-Qed.
-
-(** Pmult_nat permutes with multiplication *)
-
-Lemma Pmult_nat_mult_permute :
- forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n.
-Proof.
-  simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n).
-  rewrite (H (n + n) m). reflexivity.
-  intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H.
-  trivial.
-Qed.
-
-Lemma Pmult_nat_2_mult_2_permute :
- forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1.
-Proof.
-  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.
-Qed.
-
-Lemma Pmult_nat_4_mult_2_permute :
- forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2.
-Proof.
-  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.
-Qed.
-
-(** Mapping of xH, xO and xI through [nat_of_P] *)
-
-Lemma nat_of_P_xH : nat_of_P 1 = 1.
-Proof.
-  reflexivity.
-Qed.
-
-Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p.
-Proof.
-  intros.
-  change 2 with (nat_of_P 2).
-  rewrite <- nat_of_P_mult_morphism.
-  f_equal.
-Qed.
-
-Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p).
-Proof.
-  intros.
-  change 2 with (nat_of_P 2).
-  rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism.
-  f_equal.
-Qed.
-
-(**********************************************************************)
-(** Properties of the shifted injection from Peano natural numbers to
-    binary positive numbers *)
-
-(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *)
-
-Theorem nat_of_P_o_P_of_succ_nat_eq_succ :
- forall n:nat, nat_of_P (P_of_succ_nat n) = S n.
-Proof.
-induction n as [|n H].
-reflexivity.
-simpl; rewrite nat_of_P_succ_morphism, H; auto.
-Qed.
-
-(** Miscellaneous lemmas on [P_of_succ_nat] *)
-
-Lemma ZL3 :
- forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n).
-Proof.
-induction n as [| n H]; simpl;
- [ auto with arith
- | rewrite plus_comm; simpl; rewrite H;
-    rewrite xO_succ_permute; auto with arith ].
-Qed.
-
-Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n).
-Proof.
-induction n as [| n H]; simpl;
- [ auto with arith
- | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H;
-    auto with arith ].
-Qed.
-
-(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *)
-
-Theorem P_of_succ_nat_o_nat_of_P_eq_succ :
- forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p.
-Proof.
-intros.
-apply nat_of_P_inj.
-rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto.
-Qed.
-
-(** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity
-    on [positive] *)
-
-Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id :
- forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p.
-Proof.
-intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto.
-Qed.
-
-(**********************************************************************)
-(** Extra properties of the injection from binary positive numbers to Peano
-    natural numbers *)
-
-(** [nat_of_P] is a morphism for subtraction on positive numbers *)
-
-Theorem nat_of_P_minus_morphism :
- forall p q:positive,
-   (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.
-Proof.
-intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r;
- [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith
- | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ].
-Qed.
-
-
-Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p.
-Proof.
-intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1;
- rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S;
- apply le_minus.
-Qed.
-
-Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q).
-Proof.
-intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q);
- intros k H; rewrite H; rewrite plus_comm; simpl in |- *;
- apply le_n_S; apply le_plus_r.
-Qed.
-
-(** Comparison and subtraction *)
-
-Lemma Pcompare_minus_r :
- forall p q r:positive,
-   (q ?= p) Eq = Lt ->
-   (r ?= p) Eq = Gt ->
-   (r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt.
-Proof.
-intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
- rewrite nat_of_P_minus_morphism;
- [ rewrite nat_of_P_minus_morphism;
-    [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r;
-       [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);
-          rewrite plus_assoc; rewrite le_plus_minus_r;
-          [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l;
-             apply nat_of_P_lt_Lt_compare_morphism;
-             assumption
-          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-             apply ZC1; assumption ]
-       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
-          assumption ]
-    | assumption ]
- | assumption ].
-Qed.
-
-Lemma Pcompare_minus_l :
- forall p q r:positive,
-   (q ?= p) Eq = Lt ->
-   (p ?= r) Eq = Gt ->
-   (q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt.
-Proof.
-intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
- rewrite nat_of_P_minus_morphism;
- [ rewrite nat_of_P_minus_morphism;
-    [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z);
-       rewrite le_plus_minus_r;
-       [ rewrite le_plus_minus_r;
-          [ apply nat_of_P_lt_Lt_compare_morphism; assumption
-          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-             apply ZC1; assumption ]
-       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
-          assumption ]
-    | assumption ]
- | assumption ].
-Qed.
-
-(** Distributivity of multiplication over subtraction *)
-
-Theorem Pmult_minus_distr_l :
- forall p q r:positive,
-   (q ?= r) Eq = Gt ->
-   (p * (q - r) = p * q - p * r)%positive.
-Proof.
-intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism;
- rewrite nat_of_P_minus_morphism;
- [ rewrite nat_of_P_minus_morphism;
-    [ do 2 rewrite nat_of_P_mult_morphism;
-       do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r
-    | apply nat_of_P_gt_Gt_compare_complement_morphism;
-       do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *;
-       elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l;
-       exact (nat_of_P_gt_Gt_compare_morphism y z H) ]
- | assumption ].
-Qed.
diff --git a/theories/NArith/Psqrt.v b/theories/NArith/Psqrt.v
deleted file mode 100644
index 1d85f14a2..000000000
--- a/theories/NArith/Psqrt.v
+++ /dev/null
@@ -1,123 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import BinPos.
-
-Open Scope positive_scope.
-
-Definition Pleb x y :=
- match Pcompare x y Eq with Gt => false | _ => true end.
-
-(** A Square Root function for positive numbers *)
-
-(** We procede by blocks of two digits : if p is written qbb'
-    then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1.
-    For deciding easily in which case we are, we store the remainder
-    (as a positive_mask, since it can be null).
-    Instead of copy-pasting the following code four times, we
-    factorize as an auxiliary function, with f and g being either
-    xO or xI depending of the initial digits.
-    NB: (Pminus_mask (g (f 1)) 4) is a hack, morally it's g (f 0).
-*)
-
-Definition Psqrtrem_step (f g:positive->positive) p :=
- match p with
-  | (s, IsPos r) =>
-    let s' := s~0~1 in
-    let r' := g (f r) in
-    if Pleb s' r' then (s~1, Pminus_mask r' s')
-    else (s~0, IsPos r')
-  | (s,_)  => (s~0, Pminus_mask (g (f 1)) 4)
- end.
-
-Fixpoint Psqrtrem p : positive * positive_mask :=
- match p with
-  | 1 => (1,IsNul)
-  | 2 => (1,IsPos 1)
-  | 3 => (1,IsPos 2)
-  | p~0~0 => Psqrtrem_step xO xO (Psqrtrem p)
-  | p~0~1 => Psqrtrem_step xO xI (Psqrtrem p)
-  | p~1~0 => Psqrtrem_step xI xO (Psqrtrem p)
-  | p~1~1 => Psqrtrem_step xI xI (Psqrtrem p)
- end.
-
-Definition Psqrt p := fst (Psqrtrem p).
-
-(** An inductive relation for specifying sqrt results *)
-
-Inductive PSQRT : positive*positive_mask -> positive -> Prop :=
- | PSQRT_exact : forall s x, x=s*s -> PSQRT (s,IsNul) x
- | PSQRT_approx : forall s r x, x=s*s+r -> r <= s~0 -> PSQRT (s,IsPos r) x.
-
-(** Correctness proofs *)
-
-Lemma Psqrtrem_step_spec : forall f g p x,
- (f=xO \/ f=xI) -> (g=xO \/ g=xI) ->
- PSQRT p x -> PSQRT (Psqrtrem_step f g p) (g (f x)).
-Proof.
-intros f g _ _ Hf Hg [ s _ -> | s r _ -> Hr ].
-(* exact *)
-unfold Psqrtrem_step.
-destruct Hf,Hg; subst; simpl Pminus_mask;
- constructor; try discriminate; now rewrite Psquare_xO.
-(* approx *)
-assert (Hfg : forall p q, g (f (p+q)) = p~0~0 + g (f q))
- by (intros; destruct Hf, Hg; now subst).
-unfold Psqrtrem_step. unfold Pleb.
-case Pcompare_spec; [intros EQ | intros LT | intros GT].
-(* - EQ *)
-rewrite <- EQ. rewrite Pminus_mask_diag.
-destruct Hg; subst g; try discriminate.
-destruct Hf; subst f; try discriminate.
-injection EQ; clear EQ; intros <-.
-constructor. now rewrite Psquare_xI.
-(* - LT *)
-destruct (Pminus_mask_Gt (g (f r)) (s~0~1)) as (y & -> & H & _).
-change Eq with (CompOpp Eq). now rewrite <- Pcompare_antisym, LT.
-constructor.
-rewrite Hfg, <- H. now rewrite Psquare_xI, Pplus_assoc.
-apply Ple_lteq, Pcompare_p_Sq in Hr; change (r < s~1) in Hr.
-apply Ple_lteq, Pcompare_p_Sq; change (y < s~1~1).
-apply Pplus_lt_mono_l with (s~0~1).
-rewrite H. simpl. rewrite Pplus_carry_spec, Pplus_diag. simpl.
-set (s1:=s~1) in *; clearbody s1.
-destruct Hf,Hg; subst; red; simpl;
-  apply Hr || apply Pcompare_eq_Lt, Hr.
-(* - GT *)
-constructor.
-rewrite Hfg. now rewrite Psquare_xO.
-apply Ple_lteq, Pcompare_p_Sq, GT.
-Qed.
-
-Lemma Psqrtrem_spec : forall p, PSQRT (Psqrtrem p) p.
-Proof.
-fix 1.
- destruct p; try destruct p; try (constructor; easy);
-  apply Psqrtrem_step_spec; auto.
-Qed.
-
-Lemma Psqrt_spec : forall p,
- let s := Psqrt p in s*s <= p < (Psucc s)*(Psucc s).
-Proof.
- intros p. simpl.
- assert (H:=Psqrtrem_spec p).
- unfold Psqrt in *. destruct Psqrtrem as (s,rm); simpl.
- inversion_clear H; subst.
- (* exact *)
- split. red. rewrite Pcompare_refl. discriminate.
-  apply Pmult_lt_mono; apply Pcompare_p_Sp.
- (* approx *)
- split.
- apply Ple_lteq; left. apply Plt_plus_r.
- rewrite (Pplus_one_succ_l).
- rewrite Pmult_plus_distr_r, !Pmult_plus_distr_l.
- rewrite !Pmult_1_r. simpl (1*s).
- rewrite <- Pplus_assoc, (Pplus_assoc s s), Pplus_diag, Pplus_assoc.
- rewrite (Pplus_comm (_+_)). apply Pplus_lt_mono_l.
- rewrite <- Pplus_one_succ_l. now apply Pcompare_p_Sq, Ple_lteq.
-Qed.
diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex
index 83eed970e..bf39bc36c 100644
--- a/theories/NArith/intro.tex
+++ b/theories/NArith/intro.tex
@@ -1,4 +1,4 @@
-\section{Binary positive and non negative integers : NArith}\label{NArith}
+\section{Binary natural numbers : NArith}\label{NArith}
 
 Here are defined various arithmetical notions and their properties,
 similar to those of {\tt Arith}.
diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget
index 0caf0b249..1797b25e4 100644
--- a/theories/NArith/vo.itarget
+++ b/theories/NArith/vo.itarget
@@ -1,13 +1,8 @@
 BinNat.vo
-BinPos.vo
 NArith.vo
 Ndec.vo
 Ndigits.vo
 Ndist.vo
 Nnat.vo
 Ndiv_def.vo
-Pnat.vo
-POrderedType.vo
-Pminmax.vo
-Psqrt.vo
 Nsqrt_def.vo