Modularization of BinInt, related fixes in the stdlib

 All the functions about Z is now in a separated file BinIntDef,
 which is Included in BinInt.Z. This BinInt.Z directly
 implements ZAxiomsSig, and instantiates derived properties ZProp.

 Note that we refer to Z instead of t inside BinInt.Z,
 otherwise ring breaks later on @eq Z.t

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

25 files changed, 1960 insertions, 1476 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 61885951d..b9ae45110 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -8,7 +8,9 @@
 (************************************************************************)
 
 Require Export BinNums BinPos Pnat.
-Require Import BinNat Plus Mult.
+Require Import BinNat Bool Plus Mult Equalities GenericMinMax
+ ZAxioms ZProperties.
+Require BinIntDef.
 
 (***********************************************************)
 (** * Binary Integers *)
@@ -21,1024 +23,1467 @@ Require Import BinNat Plus Mult.
 
 Local Open Scope Z_scope.
 
-(*************************************)
-(** * Basic operations *)
-
-(** ** Subtraction of positive into Z *)
-
-Definition Zdouble_plus_one (x:Z) :=
-  match x with
-    | Z0 => Zpos 1
-    | Zpos p => Zpos p~1
-    | Zneg p => Zneg (Pdouble_minus_one p)
-  end.
-
-Definition Zdouble_minus_one (x:Z) :=
-  match x with
-    | Z0 => Zneg 1
-    | Zneg p => Zneg p~1
-    | Zpos p => Zpos (Pdouble_minus_one p)
-  end.
-
-Definition Zdouble (x:Z) :=
-  match x with
-    | Z0 => Z0
-    | Zpos p => Zpos p~0
-    | Zneg p => Zneg p~0
-  end.
-
-Fixpoint ZPminus (x y:positive) {struct y} : Z :=
-  match x, y with
-    | p~1, q~1 => Zdouble (ZPminus p q)
-    | p~1, q~0 => Zdouble_plus_one (ZPminus p q)
-    | p~1, 1 => Zpos p~0
-    | p~0, q~1 => Zdouble_minus_one (ZPminus p q)
-    | p~0, q~0 => Zdouble (ZPminus p q)
-    | p~0, 1 => Zpos (Pdouble_minus_one p)
-    | 1, q~1 => Zneg q~0
-    | 1, q~0 => Zneg (Pdouble_minus_one q)
-    | 1, 1 => Z0
-  end%positive.
-
-(** ** Addition on integers *)
-
-Definition Zplus (x y:Z) :=
-  match x, y with
-    | Z0, y => y
-    | Zpos x', Z0 => Zpos x'
-    | Zneg x', Z0 => Zneg x'
-    | Zpos x', Zpos y' => Zpos (x' + y')
-    | Zpos x', Zneg y' =>
-      match (x' ?= y')%positive with
-	| Eq => Z0
-	| Lt => Zneg (y' - x')
-	| Gt => Zpos (x' - y')
-      end
-    | Zneg x', Zpos y' =>
-      match (x' ?= y')%positive with
-	| Eq => Z0
-	| Lt => Zpos (y' - x')
-	| Gt => Zneg (x' - y')
-      end
-    | Zneg x', Zneg y' => Zneg (x' + y')
-  end.
-
-Infix "+" := Zplus : Z_scope.
-
-(** ** Opposite *)
-
-Definition Zopp (x:Z) :=
-  match x with
-    | Z0 => Z0
-    | Zpos x => Zneg x
-    | Zneg x => Zpos x
-  end.
-
-Notation "- x" := (Zopp x) : Z_scope.
-
-(** ** Successor on integers *)
-
-Definition Zsucc (x:Z) := (x + Zpos 1)%Z.
-
-(** ** Predecessor on integers *)
-
-Definition Zpred (x:Z) := (x + Zneg 1)%Z.
-
-(** ** Subtraction on integers *)
-
-Definition Zminus (m n:Z) := (m + - n)%Z.
-
-Infix "-" := Zminus : Z_scope.
-
-(** ** Multiplication on integers *)
-
-Definition Zmult (x y:Z) :=
-  match x, y with
-    | Z0, _ => Z0
-    | _, Z0 => Z0
-    | Zpos x', Zpos y' => Zpos (x' * y')
-    | Zpos x', Zneg y' => Zneg (x' * y')
-    | Zneg x', Zpos y' => Zneg (x' * y')
-    | Zneg x', Zneg y' => Zpos (x' * y')
-  end.
-
-Infix "*" := Zmult : Z_scope.
-
-(** ** Comparison of integers *)
-
-Definition Zcompare (x y:Z) :=
-  match x, y with
-    | Z0, Z0 => Eq
-    | Z0, Zpos y' => Lt
-    | Z0, Zneg y' => Gt
-    | Zpos x', Z0 => Gt
-    | Zpos x', Zpos y' => (x' ?= y')%positive
-    | Zpos x', Zneg y' => Gt
-    | Zneg x', Z0 => Lt
-    | Zneg x', Zpos y' => Lt
-    | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive)
-  end.
-
-Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
+(** Every definitions and early properties about binary integers
+    are placed in a module [Z] for qualification purpose. *)
 
-Ltac elim_compare com1 com2 :=
-  case (Dcompare (com1 ?= com2)%Z);
-    [ idtac | let x := fresh "H" in
-      (intro x; case x; clear x) ].
+Module Z
+ <: ZAxiomsSig
+ <: UsualOrderedTypeFull
+ <: UsualDecidableTypeFull
+ <: TotalOrder.
+
+(** * Definitions of operations, now in a separate file *)
+
+Include BinIntDef.Z.
+
+(** * Logic Predicates *)
+
+Definition eq := @Logic.eq Z.
+Definition eq_equiv := @eq_equivalence Z.
+
+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 "<=" := le : Z_scope.
+Infix "<" := lt : Z_scope.
+Infix ">=" := ge : Z_scope.
+Infix ">" := gt : Z_scope.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
+Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 
-(** ** Sign function *)
-
-Definition Zsgn (z:Z) : Z :=
-  match z with
-    | Z0 => Z0
-    | Zpos p => Zpos 1
-    | Zneg p => Zneg 1
-  end.
-
-(** ** Direct, easier to handle variants of successor and addition *)
-
-Definition Zsucc' (x:Z) :=
-  match x with
-    | Z0 => Zpos 1
-    | Zpos x' => Zpos (Psucc x')
-    | Zneg x' => ZPminus 1 x'
-  end.
-
-Definition Zpred' (x:Z) :=
-  match x with
-    | Z0 => Zneg 1
-    | Zpos x' => ZPminus x' 1
-    | Zneg x' => Zneg (Psucc x')
-  end.
-
-Definition Zplus' (x y:Z) :=
-  match x, y with
-    | Z0, y => y
-    | x, Z0 => x
-    | Zpos x', Zpos y' => Zpos (x' + y')
-    | Zpos x', Zneg y' => ZPminus x' y'
-    | Zneg x', Zpos y' => ZPminus y' x'
-    | Zneg x', Zneg y' => Zneg (x' + y')
-  end.
-
-(**********************************************************************)
-(** ** Inductive specification of Z *)
-
-Theorem Zind :
-  forall P:Z -> Prop,
-    P Z0 ->
-    (forall x:Z, P x -> P (Zsucc' x)) ->
-    (forall x:Z, P x -> P (Zpred' x)) -> forall n:Z, P n.
-Proof.
-  intros P H0 Hs Hp z; destruct z.
-  assumption.
-  apply Pind with (P := fun p => P (Zpos p)).
-    change (P (Zsucc' Z0)); apply Hs; apply H0.
-    intro n; exact (Hs (Zpos n)).
-  apply Pind with (P := fun p => P (Zneg p)).
-    change (P (Zpred' Z0)); apply Hp; apply H0.
-    intro n; exact (Hp (Zneg n)).
-Qed.
-
-(**********************************************************************)
-(** * Misc properties about binary integer operations *)
-
-(**********************************************************************)
-(** ** Properties of opposite on binary integer numbers *)
-
-Theorem Zopp_0 : Zopp Z0 = Z0.
+Definition divide x y := exists z, x*z = y.
+Notation "( x | y )" := (divide x y) (at level 0).
+
+Definition Even a := exists b, a = 2*b.
+Definition Odd a := exists b, a = 2*b+1.
+
+(** * Decidability of equality. *)
+
+Definition eq_dec (x y : Z) : {x = y} + {x <> y}.
 Proof.
-  reflexivity.
+ decide equality; apply Pos.eq_dec.
+Defined.
+
+(** * Equivalence with alternative [add'] [succ'] [pred'] *)
+
+(** ** Caracterisation of [pos_sub] *)
+
+Lemma pos_sub_spec p q : pos_sub p q = Zpos p + Zneg q.
+Proof.
+ revert q. induction p; destruct q; simpl; trivial;
+ rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI,
+  ?Pos.compare_xI_xO, ?Pos.compare_xO_xO, IHp; simpl;
+ case Pos.compare_spec; intros; simpl; trivial;
+  (now rewrite Pos.sub_xI_xI) || (now rewrite Pos.sub_xO_xO) ||
+  (now rewrite Pos.sub_xO_xI) || (now rewrite Pos.sub_xI_xO) ||
+  subst; unfold Pos.sub; simpl; now rewrite Pos.sub_mask_diag.
 Qed.
 
-Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
+Lemma add_add' n m : n + m = add' n m.
 Proof.
-  reflexivity.
+ symmetry.
+ destruct n as [|n|n], m as [|m|m]; simpl add'; rewrite ?pos_sub_spec;
+  trivial.
+ simpl. rewrite Pos.compare_antisym. now case Pos.compare.
 Qed.
 
-(** [opp] is involutive *)
+Lemma succ_succ' n : succ n = succ' n.
+Proof.
+ unfold succ. rewrite add_add'. destruct n; trivial.
+ simpl. f_equal. apply Pos.add_1_r.
+Qed.
 
-Theorem Zopp_involutive : forall n:Z, - - n = n.
+Lemma pred_pred' n : pred n = pred' n.
 Proof.
-  intro x; destruct x; reflexivity.
+ unfold pred. rewrite add_add'. destruct n; trivial.
+ simpl. f_equal. apply Pos.add_1_r.
 Qed.
 
-(** Injectivity of the opposite *)
+(** * Results concerning [Zpos] and [Zneg] and the operators *)
+
+Lemma opp_Zneg p : - Zneg p = Zpos p.
+Proof.
+ reflexivity.
+Qed.
 
-Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m.
+Lemma opp_Zpos p : - Zpos p = Zneg p.
 Proof.
-  intros x y; case x; case y; simpl; intros;
-    [ trivial
-      | discriminate H
-      | discriminate H
-      | discriminate H
-      | simplify_eq H; intro E; rewrite E; trivial
-      | discriminate H
-      | discriminate H
-      | discriminate H
-      | simplify_eq H; intro E; rewrite E; trivial ].
+ reflexivity.
 Qed.
 
-(**********************************************************************)
-(** ** Other properties of binary integer numbers *)
+Lemma succ_Zpos p : succ (Zpos p) = Zpos (Pos.succ p).
+Proof.
+ simpl. f_equal. apply Pos.add_1_r.
+Qed.
 
-Lemma ZL0 : 2%nat = (1 + 1)%nat.
+Lemma add_Zpos p q : Zpos p + Zpos q = Zpos (p+q).
 Proof.
-  reflexivity.
+ reflexivity.
 Qed.
 
-(**********************************************************************)
-(** * Properties of the addition on integers *)
+Lemma add_Zneg p q : Zneg p + Zneg q = Zneg (p+q).
+Proof.
+ reflexivity.
+Qed.
 
-(** ** Zero is left neutral for addition *)
+Lemma sub_Zpos n m : (n < m)%positive -> Zpos m - Zpos n = Zpos (m-n).
+Proof.
+ intros H. simpl. now rewrite Pos.compare_antisym, H.
+Qed.
 
-Theorem Zplus_0_l : forall n:Z, Z0 + n = n.
+Lemma mul_Zpos (p q : positive) : Zpos p * Zpos q = Zpos (p*q).
 Proof.
-  intro x; destruct x; reflexivity.
+ reflexivity.
 Qed.
 
-(** ** Zero is right neutral for addition *)
+Lemma pow_Zpos p q : (Zpos p)^(Zpos q) = Zpos (p^q).
+Proof.
+ unfold Pos.pow, pow, pow_pos.
+ symmetry. now apply Pos.iter_swap_gen.
+Qed.
 
-Theorem Zplus_0_r : forall n:Z, n + Z0 = n.
+Lemma inj_Zpos p q : Zpos p = Zpos q <-> p = q.
 Proof.
-  intro x; destruct x; reflexivity.
+ split; intros H. now injection H. now f_equal.
 Qed.
 
-(** ** Addition is commutative *)
+Lemma inj_Zneg p q : Zneg p = Zneg q <-> p = q.
+Proof.
+ split; intros H. now injection H. now f_equal.
+Qed.
 
-Theorem Zplus_comm : forall n m:Z, n + m = m + n.
+Lemma pos_xI p : Zpos p~1 = 2 * Zpos p + 1.
 Proof.
-  induction n as [|p|p]; intros [|q|q]; simpl; try reflexivity.
-  rewrite Pplus_comm; reflexivity.
-  rewrite Pos.compare_antisym. now case Pcompare_spec.
-  rewrite Pos.compare_antisym. now case Pcompare_spec.
-  rewrite Pplus_comm; reflexivity.
+ reflexivity.
 Qed.
 
-(** ** Opposite distributes over addition *)
+Lemma pos_xO p : Zpos p~0 = 2 * Zpos p.
+Proof.
+ reflexivity.
+Qed.
 
-Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
+Lemma neg_xI p : Zneg p~1 = 2 * Zneg p - 1.
 Proof.
-  intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
-    simpl; reflexivity || destruct ((p ?= q)%positive);
-      reflexivity.
+ reflexivity.
 Qed.
 
-Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n).
+Lemma neg_xO p : Zneg p~0 = 2 * Zneg p.
 Proof.
-intro; unfold Zsucc; now rewrite Zopp_plus_distr.
+ reflexivity.
 Qed.
 
-(** ** Opposite is inverse for addition *)
+(** In the following module, we group results that are needed now
+  to prove specifications of operations, but will also be provided
+  later by the generic functor of properties. *)
+
+Module Import BootStrap.
 
-Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
+(** * Properties of addition *)
+
+(** ** Zero is neutral for addition *)
+
+Lemma add_0_r n : n + 0 = n.
 Proof.
-  intro x; destruct x as [| p| p]; simpl;
-    [ reflexivity
-      | rewrite (Pcompare_refl p); reflexivity
-      | rewrite (Pcompare_refl p); reflexivity ].
+ now destruct n.
 Qed.
 
-Theorem Zplus_opp_l : forall n:Z, - n + n = Z0.
+(** ** Addition is commutative *)
+
+Lemma add_comm n m : n + m = m + n.
 Proof.
-  intro; rewrite Zplus_comm; apply Zplus_opp_r.
+ rewrite !add_add'.
+ destruct n, m; simpl; trivial; now rewrite Pos.add_comm.
 Qed.
 
-Hint Local Resolve Zplus_0_l Zplus_0_r.
+(** ** Opposite distributes over addition *)
+
+Lemma opp_add_distr n m : - (n + m) = - n + - m.
+Proof.
+  destruct n, m; simpl; trivial; now case Pos.compare_spec.
+Qed.
 
 (** ** Addition is associative *)
 
-Lemma weak_assoc :
-  forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
+Lemma add_assoc_pos (p q:positive)(n:Z) :
+  Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
 Proof.
- intros x y [|z|z]; simpl; trivial.
- now rewrite Pplus_assoc.
- case (Pcompare_spec y z); intros E0.
+ destruct n as [|n|n]; simpl; trivial.
+ now rewrite Pos.add_assoc.
+ case Pos.compare_spec; intros E0.
  (* y = z *)
  subst.
- assert (H := Plt_plus_r z x). rewrite Pplus_comm in H. apply ZC2 in H.
- now rewrite H, Pplus_minus_eq.
+ assert (H := Pos.lt_add_r n p).
+ rewrite Pos.add_comm in H. apply Pos.lt_gt in H.
+ now rewrite H, Pos.add_sub.
  (* y < z *)
- assert (Hz : (z = (z-y)+y)%positive) by (now rewrite Pos.sub_add).
- pattern z at 4. rewrite Hz, Pplus_compare_mono_r.
- case Pcompare_spec; intros E1; trivial; f_equal.
- symmetry. rewrite Pplus_comm. apply Pminus_plus_distr.
- rewrite Hz, Pplus_comm. now apply Pplus_lt_mono_r.
- apply Pminus_minus_distr; trivial.
+ assert (Hz : (n = (n-q)+q)%positive) by (now rewrite Pos.sub_add).
+ rewrite Hz at 4. rewrite Pos.add_compare_mono_r.
+ case Pos.compare_spec; intros E1; trivial; f_equal.
+ symmetry. rewrite Pos.add_comm. apply Pos.sub_add_distr.
+ rewrite Hz, Pos.add_comm. now apply Pos.add_lt_mono_r.
+ apply Pos.sub_sub_distr; trivial.
  (* z < y *)
- assert (LT : (z < x + y)%positive).
-  rewrite Pplus_comm. apply Plt_trans with y; trivial using Plt_plus_r.
- apply ZC2 in LT. rewrite LT. f_equal.
- now apply Pplus_minus_assoc.
+ assert (LT : (n < p + q)%positive).
+  apply Pos.lt_trans with q; trivial. rewrite Pos.add_comm. apply Pos.lt_add_r.
+ apply Pos.lt_gt in LT. rewrite LT. f_equal.
+ now apply Pos.add_sub_assoc.
+Qed.
+
+Lemma add_assoc n m p : n + (m + p) = n + m + p.
+Proof.
+ destruct n as [|x|x], m as [|y|y], p as [|z|z]; trivial.
+ apply add_assoc_pos.
+ apply add_assoc_pos.
+ now rewrite !add_0_r.
+ rewrite 2 (add_comm _ (Zpos z)), 2 add_assoc_pos.
+  f_equal; apply add_comm.
+ rewrite <- !opp_Zpos, <- (opp_Zneg x), <- !opp_add_distr. f_equal.
+  rewrite 2 (add_comm (Zneg x)), 2 (add_comm _ (Zpos z)).
+  now rewrite add_assoc_pos.
+ now rewrite !add_0_r.
+ rewrite 2 (add_comm (Zneg x)), 2 (add_comm _ (Zpos z)).
+  now rewrite add_assoc_pos.
+ rewrite <- !opp_Zpos, <- (opp_Zneg y), <- !opp_add_distr. f_equal.
+ rewrite 2 (add_comm _ (Zpos z)), 2 add_assoc_pos.
+  f_equal; apply add_comm.
+ rewrite <- !opp_Zpos, <- (opp_Zneg z), <- !opp_add_distr. f_equal.
+  apply add_assoc_pos.
+ rewrite <- !opp_Zpos, <- !opp_add_distr. f_equal.
+  apply add_assoc_pos.
+Qed.
+
+(** ** Subtraction and successor *)
+
+Lemma sub_succ_l n m : succ n - m = succ (n - m).
+Proof.
+ unfold sub, succ. now rewrite <- 2 add_assoc, (add_comm 1).
 Qed.
 
-Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p.
+(** ** Opposite is inverse for addition *)
+
+Lemma add_opp_diag_r n : n + - n = 0.
 Proof.
- intros [|x|x] [|y|y] [|z|z]; trivial.
- apply weak_assoc.
- apply weak_assoc.
- now rewrite !Zplus_0_r.
- rewrite 2 (Zplus_comm _ (Zpos z)), 2 weak_assoc.
-  f_equal; apply Zplus_comm.
- apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
-  rewrite 2 (Zplus_comm (-Zpos x)), 2 (Zplus_comm _ (Zpos z)).
-  now rewrite weak_assoc.
- now rewrite !Zplus_0_r.
- rewrite 2 (Zplus_comm (Zneg x)), 2 (Zplus_comm _ (Zpos z)).
-  now rewrite weak_assoc.
- apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
- rewrite 2 (Zplus_comm _ (Zpos z)), 2 weak_assoc.
-  f_equal; apply Zplus_comm.
- apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
-  apply weak_assoc.
- apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg.
-  apply weak_assoc.
+ destruct n; simpl; trivial; now rewrite Pos.compare_refl.
 Qed.
 
-Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p).
+Lemma add_opp_diag_l n : - n + n = 0.
 Proof.
-  intros; symmetry ; apply Zplus_assoc.
+ rewrite add_comm. apply add_opp_diag_r.
 Qed.
 
-(** ** Associativity mixed with commutativity *)
+(** ** Commutativity of multiplication *)
 
-Theorem Zplus_permute : forall n m p:Z, n + (m + p) = m + (n + p).
+Lemma mul_comm n m : n * m = m * n.
 Proof.
-  intros n m p; rewrite Zplus_comm; rewrite <- Zplus_assoc;
-    rewrite (Zplus_comm p n); trivial with arith.
+ destruct n, m; simpl; trivial; f_equal; apply Pos.mul_comm.
 Qed.
 
-(** ** Addition simplifies *)
+(** ** Associativity of multiplication *)
 
-Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
-  intros n m p H; cut (- n + (n + m) = - n + (n + p));
-    [ do 2 rewrite Zplus_assoc; rewrite (Zplus_comm (- n) n);
-      rewrite Zplus_opp_r; simpl; trivial with arith
-      | rewrite H; trivial with arith ].
+Lemma mul_assoc n m p : n * (m * p) = n * m * p.
+Proof.
+ destruct n, m, p; simpl; trivial; f_equal; apply Pos.mul_assoc.
 Qed.
 
-(** ** Addition and successor permutes *)
+(** Multiplication and constants *)
 
-Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
+Lemma mul_1_l n : 1 * n = n.
 Proof.
-  intros x y; unfold Zsucc; rewrite (Zplus_comm (x + y));
-    rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1));
-      trivial with arith.
+ now destruct n.
 Qed.
 
-Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
+Lemma mul_1_r n : n * 1 = n.
 Proof.
-  intros n m; unfold Zsucc; rewrite Zplus_assoc; trivial with arith.
+ destruct n; simpl; now rewrite ?Pos.mul_1_r.
 Qed.
 
-Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
+(** ** Multiplication and Opposite *)
 
-Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
+Lemma mul_opp_l n m : - n * m = - (n * m).
 Proof.
-  unfold Zsucc; intros n m; rewrite <- Zplus_assoc;
-    rewrite (Zplus_comm (Zpos 1)); trivial with arith.
+ now destruct n, m.
 Qed.
 
-(** ** Misc properties, usually redundant or non natural *)
+Lemma mul_opp_r n m : n * - m = - (n * m).
+Proof.
+ now destruct n, m.
+Qed.
 
-Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0.
+Lemma mul_opp_opp n m : - n * - m = n * m.
 Proof.
-  symmetry ; apply Zplus_0_r.
+ now destruct n, m.
 Qed.
 
-Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m.
+Lemma mul_opp_comm n m : - n * m = n * - m.
 Proof.
-  intros n m; rewrite Zplus_0_r; intro; assumption.
+ now destruct n, m.
 Qed.
 
-Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m.
+(** ** Distributivity of multiplication over addition *)
+
+Lemma mul_add_distr_pos (p:positive) n m :
+ Zpos p * (n + m) = Zpos p * n + Zpos p * m.
 Proof.
-  intros n m; rewrite Zplus_0_r; intro; assumption.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial;
+ rewrite ?Pos.mul_compare_mono_l; try case Pos.compare_spec; intros;
+ now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l.
 Qed.
 
-Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q.
+Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
 Proof.
-  intros; rewrite H; rewrite H0; reflexivity.
+ destruct n as [|n|n]. trivial.
+ apply mul_add_distr_pos.
+ rewrite <- opp_Zpos, !mul_opp_l, <- opp_add_distr. f_equal.
+ apply mul_add_distr_pos.
 Qed.
 
-Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m).
+Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
 Proof.
-  intros x y z.
-  rewrite <- (Zplus_assoc x).
-  rewrite (Zplus_assoc (- z)).
-  rewrite Zplus_opp_l.
-  reflexivity.
+ rewrite !(mul_comm _ p). apply mul_add_distr_l.
 Qed.
 
-(************************************************************************)
-(** * Properties of successor and predecessor on binary integer numbers *)
+End BootStrap.
+
+(** * Proofs of specifications *)
 
-Theorem Zsucc_discr : forall n:Z, n <> Zsucc n.
+(** ** Specification of constants *)
+
+Lemma one_succ : 1 = succ 0.
 Proof.
-  intros n; cut (Z0 <> Zpos 1);
-    [ unfold not; intros H1 H2; apply H1; apply (Zplus_reg_l n);
-      rewrite Zplus_0_r; exact H2
-      | discriminate ].
+reflexivity.
 Qed.
 
-Theorem Zpos_succ_morphism :
-  forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p).
+Lemma two_succ : 2 = succ 1.
 Proof.
-  intro; rewrite Pplus_one_succ_r; unfold Zsucc; simpl;
-    trivial with arith.
+reflexivity.
 Qed.
 
-(** successor and predecessor are inverse functions *)
+(** ** Specification of addition *)
 
-Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
+Lemma add_0_l n : 0 + n = n.
 Proof.
-  intros n; unfold Zsucc, Zpred; rewrite <- Zplus_assoc; simpl;
-    rewrite Zplus_0_r; trivial with arith.
+ now destruct n.
 Qed.
 
-Hint Immediate Zsucc_pred: zarith.
+Lemma add_succ_l n m : succ n + m = succ (n + m).
+Proof.
+ unfold succ. now rewrite 2 (add_comm _ 1), add_assoc.
+Qed.
+
+(** ** Specification of opposite *)
 
-Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).
+Lemma opp_0 : -0 = 0.
 Proof.
-  intros m; unfold Zpred, Zsucc; rewrite <- Zplus_assoc; simpl;
-    rewrite Zplus_comm; auto with arith.
+ reflexivity.
 Qed.
 
-Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m.
+Lemma opp_succ n : -(succ n) = pred (-n).
 Proof.
-  intros n m H.
-  change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m);
-    do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1));
-      unfold Zsucc in H; rewrite H; trivial with arith.
+ unfold succ, pred. destruct n; simpl; trivial. now case Pos.compare_spec.
 Qed.
 
-(*************************************************************************)
-(** **  Properties of the direct definition of successor and predecessor *)
+(** ** Specification of successor and predecessor *)
 
-Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.
+Lemma succ_pred n : succ (pred n) = n.
 Proof.
-destruct n as [| p | p]; simpl.
-reflexivity.
-now rewrite Pplus_one_succ_r.
-now destruct p as [q | q |].
+ unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r.
 Qed.
 
-Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n.
+Lemma pred_succ n : pred (succ n) = n.
 Proof.
-destruct n as [| p | p]; simpl.
-reflexivity.
-now destruct p as [q | q |].
-now rewrite Pplus_one_succ_r.
+ unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r.
+Qed.
+
+(** ** Specification of subtraction *)
+
+Lemma sub_0_r n : n - 0 = n.
+Proof.
+ apply add_0_r.
 Qed.
 
-Theorem Zsucc'_inj : forall n m:Z, Zsucc' n = Zsucc' m -> n = m.
+Lemma sub_succ_r n m : n - succ m = pred (n - m).
 Proof.
-intros n m; do 2 rewrite <- Zsucc_succ'; now apply Zsucc_inj.
+ unfold sub, succ, pred. now rewrite opp_add_distr, add_assoc.
 Qed.
 
-Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n.
+(** ** Specification of multiplication *)
+
+Lemma mul_0_l n : 0 * n = 0.
 Proof.
-intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
-symmetry; apply Zsucc_pred.
+ reflexivity.
 Qed.
 
-Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
+Lemma mul_succ_l n m : succ n * m = n * m + m.
 Proof.
-intro; apply Zsucc'_inj; now rewrite Zsucc'_pred'.
+ unfold succ. now rewrite mul_add_distr_r, mul_1_l.
 Qed.
 
-Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m.
+(** ** Specification of order *)
+
+Lemma compare_refl n : (n ?= n) = Eq.
 Proof.
-intros n m H.
-rewrite <- (Zsucc'_pred' n); rewrite <- (Zsucc'_pred' m); now rewrite H.
+ destruct n; simpl; trivial; now rewrite Pos.compare_refl.
 Qed.
 
-Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n.
+Lemma compare_eq n m : (n ?= m) = Eq -> n = m.
 Proof.
-  intro x; destruct x; simpl.
-  discriminate.
-  injection; apply Psucc_discr.
-  destruct p; simpl.
-    discriminate.
-    intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
-    discriminate.
+destruct n, m; simpl; try easy; intros; f_equal.
+now apply Pos.compare_eq.
+apply Pos.compare_eq, CompOpp_inj. now rewrite H.
 Qed.
 
-(** Misc properties, usually redundant or non natural *)
+Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
+Proof.
+split; intros. now apply compare_eq. subst; now apply compare_refl.
+Qed.
 
-Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m.
+Lemma compare_antisym n m : CompOpp (n ?= m) = (m ?= n).
 Proof.
-  intros n m H; rewrite H; reflexivity.
+destruct n, m; simpl; trivial.
+symmetry. apply Pos.compare_antisym. (* TODO : quel sens ? *)
+f_equal. symmetry. apply Pos.compare_antisym.
 Qed.
 
-Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m.
+Lemma compare_sub n m : (n ?= m) = (n - m ?= 0).
 Proof.
-  unfold not; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial.
+ case Pos.compare_spec; trivial.
+ case Pos.compare_spec; trivial.
 Qed.
 
-(**********************************************************************)
-(** * Properties of subtraction on binary integer numbers *)
+Lemma compare_spec n m : CompareSpec (n=m) (n<m) (m<n) (n ?= m).
+Proof.
+ case_eq (n ?= m); intros H; constructor; trivial.
+ now apply compare_eq.
+ red. now rewrite <- compare_antisym, H.
+Qed.
 
-(** ** [minus] and [Z0] *)
+Lemma lt_irrefl n : ~ n < n.
+Proof.
+ unfold lt. now rewrite compare_refl.
+Qed.
 
-Lemma Zminus_0_r : forall n:Z, n - Z0 = n.
+Lemma lt_eq_cases n m : n <= m <-> n < m \/ n = m.
 Proof.
-  intro; unfold Zminus; simpl; rewrite Zplus_0_r;
-    trivial with arith.
+ unfold le, lt. rewrite <- compare_eq_iff.
+ case compare; now intuition.
 Qed.
 
-Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0.
+Lemma lt_succ_r n m : n < succ m <-> n<=m.
 Proof.
-  intro; symmetry ; apply Zminus_0_r.
+ unfold lt, le. rewrite compare_sub, sub_succ_r.
+ rewrite (compare_sub n m).
+ destruct (n-m) as [|[ | | ]|]; easy'.
 Qed.
 
-Lemma Zminus_diag : forall n:Z, n - n = Z0.
+(** ** Specification of boolean comparisons *)
+
+Lemma eqb_eq n m : (n =? m) = true <-> n = m.
 Proof.
-  intro; unfold Zminus; rewrite Zplus_opp_r; trivial with arith.
+ destruct n, m; simpl; try (now split).
+ rewrite inj_Zpos. apply Pos.eqb_eq.
+ rewrite inj_Zneg. apply Pos.eqb_eq.
 Qed.
 
-Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n.
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
 Proof.
-  intro; symmetry ; apply Zminus_diag.
+ unfold ltb, lt. destruct compare; easy'.
 Qed.
 
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
+Proof.
+ unfold leb, le. destruct compare; easy'.
+Qed.
 
-(** ** Relating [minus] with [plus] and [Zsucc] *)
+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 Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p.
+Lemma ltb_spec n m : BoolSpec (n<m) (m<=n) (n <? m).
 Proof.
-intros; unfold Zminus; rewrite Zopp_plus_distr; apply Zplus_assoc.
+ unfold le, lt, ltb. rewrite <- (compare_antisym n m).
+ case compare; now constructor.
 Qed.
 
-Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
+Lemma gtb_ltb n m : (n >? m) = (m <? n).
 Proof.
-  intros n m; unfold Zminus, Zsucc; rewrite (Zplus_comm n (- m));
-    rewrite <- Zplus_assoc; apply Zplus_comm.
+ unfold gtb, ltb. rewrite <- compare_antisym. now case compare.
 Qed.
 
-Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m).
+Lemma geb_leb n m : (n >=? m) = (m <=? n).
 Proof.
-intros; unfold Zsucc; now rewrite Zminus_plus_distr.
+ unfold geb, leb. rewrite <- compare_antisym. now case compare.
 Qed.
 
-Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.
+Lemma gtb_lt n m : (n >? m) = true <-> m < n.
 Proof.
-  intros n m p H; unfold Zminus; apply (Zplus_reg_l m);
-    rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc;
-      rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H;
-	trivial with arith.
+ rewrite gtb_ltb. apply ltb_lt.
 Qed.
 
-Lemma Zminus_plus : forall n m:Z, n + m - n = m.
+Lemma geb_le n m : (n >=? m) = true <-> m <= n.
 Proof.
-  intros n m; unfold Zminus; rewrite (Zplus_comm n m);
-    rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r.
+ rewrite geb_leb. apply leb_le.
 Qed.
 
-Lemma Zplus_minus : forall n m:Z, n + (m - n) = m.
+Lemma gtb_spec n m : BoolSpec (m<n) (n<=m) (n >? m).
 Proof.
-  unfold Zminus; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r;
-    apply Zplus_0_r.
+ rewrite gtb_ltb. apply ltb_spec.
 Qed.
 
-Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.
+Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m).
 Proof.
-  intros n m p; unfold Zminus; rewrite Zopp_plus_distr;
-    rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p);
-      rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith.
+ rewrite geb_leb. apply leb_spec.
 Qed.
 
-Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m).
+(** ** Specification of minimum and maximum *)
+
+Lemma max_l n m : m<=n -> max n m = n.
 Proof.
-  intros; symmetry ; apply Zminus_plus_simpl_l.
+ unfold le, max. rewrite <- (compare_antisym n m).
+ case compare; intuition.
 Qed.
 
-Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m.
+Lemma max_r n m :  n<=m -> max n m = m.
 Proof.
-  intros x y n.
-  unfold Zminus.
-  rewrite Zopp_plus_distr.
-  rewrite (Zplus_comm (- y) (- n)).
-  rewrite Zplus_assoc.
-  rewrite <- (Zplus_assoc x n (- n)).
-  rewrite (Zplus_opp_r n).
-  rewrite <- Zplus_0_r_reverse.
-  reflexivity.
+ unfold le, max. case compare_spec; intuition.
 Qed.
 
-Lemma Zpos_minus_morphism : forall a b:positive, Pos.compare a b = Lt ->
-  Zpos (b-a) = Zpos b - Zpos a.
+Lemma min_l n m : n<=m -> min n m = n.
 Proof.
-  intros.
-  simpl.
-  rewrite Pos.compare_antisym.
-  rewrite H; simpl; auto.
+ unfold le, min. case compare_spec; intuition.
+Qed.
+
+Lemma min_r n m : m<=n -> min n m = m.
+Proof.
+ unfold le, min.
+ rewrite <- (compare_antisym n m). case compare_spec; intuition.
+Qed.
+
+(** ** Specification of absolute value *)
+
+Lemma abs_eq n : 0 <= n -> abs n = n.
+Proof.
+ destruct n; trivial. now destruct 1.
+Qed.
+
+Lemma abs_neq n : n <= 0 -> abs n = - n.
+Proof.
+ destruct n; trivial. now destruct 1.
 Qed.
 
-(** ** Misc redundant properties *)
+(** ** Specification of sign *)
 
-Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
+Lemma sgn_null n : n = 0 -> sgn n = 0.
 Proof.
-  intros x y H; rewrite H; symmetry ; apply Zminus_diag_reverse.
+ intros. now subst.
 Qed.
 
-Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m.
+Lemma sgn_pos n : 0 < n -> sgn n = 1.
 Proof.
-  intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r.
+ now destruct n.
 Qed.
 
+Lemma sgn_neg n : n < 0 -> sgn n = -1.
+Proof.
+ now destruct n.
+Qed.
 
-(**********************************************************************)
-(** * Properties of multiplication on binary integer numbers *)
+(** ** Specification of power *)
 
-Theorem Zpos_mult_morphism :
-  forall p q:positive, Zpos (p*q) = Zpos p * Zpos q.
+Lemma pow_0_r n : n^0 = 1.
 Proof.
-  auto.
+ reflexivity.
 Qed.
 
-(** ** One is neutral for multiplication *)
+Lemma pow_succ_r n m : 0<=m -> n^(succ m) = n * n^m.
+Proof.
+ destruct m as [|m|m]; (now destruct 1) || (intros _); simpl; trivial.
+ unfold pow_pos. now rewrite Pos.add_comm, Pos.iter_add.
+Qed.
 
-Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n.
+Lemma pow_neg_r n m : m<0 -> n^m = 0.
 Proof.
-  intro x; destruct x; reflexivity.
+ now destruct m.
 Qed.
 
-Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n.
+(** ** Specification of square root *)
+
+Lemma sqrtrem_spec n : 0<=n ->
+ let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
 Proof.
-  intro x; destruct x; simpl; try rewrite Pmult_1_r; reflexivity.
+ destruct n. now repeat split.
+ generalize (Pos.sqrtrem_spec p). simpl.
+ destruct 1; simpl; subst; now repeat split.
+ now destruct 1.
 Qed.
 
-(** ** Zero property of multiplication *)
+Lemma sqrt_spec n : 0<=n ->
+ let s := sqrt n in s*s <= n < (succ s)*(succ s).
+Proof.
+ destruct n. now repeat split. unfold sqrt.
+ rewrite succ_Zpos. intros _. apply (Pos.sqrt_spec p).
+ now destruct 1.
+Qed.
 
-Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0.
+Lemma sqrt_neg n : n<0 -> sqrt n = 0.
 Proof.
-  intro x; destruct x; reflexivity.
+ now destruct n.
 Qed.
 
-Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0.
+Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.
 Proof.
-  intro x; destruct x; reflexivity.
+ destruct n; try reflexivity.
+ unfold sqrtrem, sqrt, Pos.sqrt.
+ destruct (Pos.sqrtrem p) as (s,r). now destruct r.
 Qed.
 
-Hint Local Resolve Zmult_0_l Zmult_0_r.
+(** ** Specification of logarithm *)
 
-Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0.
+Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)).
 Proof.
-  intro x; destruct x; reflexivity.
+ destruct n as [|[p|p|]|]; intros Hn; split; try easy; unfold log2;
+  rewrite ?succ_Zpos, pow_Zpos.
+ change (2^Pos.size p <= Pos.succ (p~0))%positive.
+ apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le.
+ apply Pos.size_gt.
+ apply Pos.size_le.
+ apply Pos.size_gt.
 Qed.
 
-(** ** Commutativity of multiplication *)
+Lemma log2_nonpos n : n<=0 -> log2 n = 0.
+Proof.
+ destruct n as [|p|p]; trivial; now destruct 1.
+Qed.
 
-Theorem Zmult_comm : forall n m:Z, n * m = m * n.
+(** Specification of parity functions *)
+
+Lemma even_spec n : even n = true <-> Even n.
 Proof.
-  intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl;
-    try rewrite (Pmult_comm p q); reflexivity.
+ split.
+ exists (div2 n). now destruct n as [|[ | | ]|[ | | ]].
+ intros (m,->). now destruct m.
 Qed.
 
-(** ** Associativity of multiplication *)
+Lemma odd_spec n : odd n = true <-> Odd n.
+Proof.
+ split.
+ exists (div2 n). destruct n as [|[ | | ]|[ | | ]]; simpl; try easy.
+ now rewrite Pos.double_succ, Pos.sub_1_r, Pos.pred_succ.
+ intros (m,->). now destruct m as [|[ | | ]|[ | | ]].
+Qed.
 
-Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p.
+(** ** Multiplication and Doubling *)
+
+Lemma double_spec n : double n = 2*n.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma succ_double_spec n : succ_double n = 2*n + 1.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma pred_double_spec n : pred_double n = 2*n - 1.
+Proof.
+ now destruct n.
+Qed.
+
+(** ** Correctness proofs for Trunc division *)
+
+Lemma pos_div_eucl_eq a b : 0 < b ->
+  let (q, r) := pos_div_eucl a b in Zpos a = q * b + r.
+Proof.
+ intros Hb.
+ induction a; unfold pos_div_eucl; fold pos_div_eucl.
+ (* ~1 *)
+ destruct pos_div_eucl as (q,r).
+ rewrite pos_xI, IHa, mul_add_distr_l, mul_assoc.
+ destruct gtb.
+ now rewrite add_assoc.
+ rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal.
+ unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r.
+ (* ~0 *)
+ destruct pos_div_eucl as (q,r).
+ rewrite (pos_xO a), IHa, mul_add_distr_l, mul_assoc.
+ destruct gtb.
+ trivial.
+ rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal.
+ unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r.
+ (* ~1 *)
+ case geb_spec; trivial.
+ intros Hb'.
+ destruct b as [|b|b]; try easy; clear Hb.
+ replace b with 1%positive; trivial.
+ apply Pos.le_antisym. apply Pos.le_1_l. now apply Pos.lt_succ_r.
+Qed.
+
+Lemma div_eucl_eq a b : b<>0 ->
+ let (q, r) := div_eucl a b in a = b * q + r.
+Proof.
+ destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial;
+  (now destruct 1) || intros _;
+  generalize (pos_div_eucl_eq a (Zpos b) (eq_refl _));
+  destruct pos_div_eucl as (q,r); rewrite <- ?opp_Zpos, mul_comm;
+  intros ->.
+ (* Zpos Zpos *)
+ trivial.
+ (* Zpos Zneg *)
+ destruct r as [ |r|r]; rewrite !mul_opp_opp; trivial;
+  rewrite mul_add_distr_l, mul_1_r, <- add_assoc; f_equal;
+  now rewrite add_assoc, add_opp_diag_r.
+ (* Zneg Zpos *)
+ rewrite (opp_add_distr _ r), <- mul_opp_r.
+ destruct r as [ |r|r]; trivial;
+  rewrite opp_add_distr, mul_add_distr_l, <- add_assoc; f_equal;
+  unfold sub; now rewrite add_assoc, mul_opp_r, mul_1_r, add_opp_diag_l.
+ (* Zneg Zneg *)
+ now rewrite opp_add_distr, <- mul_opp_l.
+Qed.
+
+Lemma div_mod a b : b<>0 -> a = b*(a/b) + (a mod b).
+Proof.
+ intros Hb. generalize (div_eucl_eq a b Hb).
+ unfold div, modulo. now destruct div_eucl.
+Qed.
+
+Lemma pos_div_eucl_bound a b : 0<b -> 0 <= snd (pos_div_eucl a b) < b.
+Proof.
+ assert (AUX : forall m p, m < Zpos (p~0) -> m - Zpos p < Zpos p).
+  intros m p. unfold lt.
+  rewrite (compare_sub m), (compare_sub _ (Zpos _)). unfold sub.
+  rewrite <- add_assoc. simpl opp; simpl (Zneg _ + _).
+  now rewrite Pos.add_diag.
+ intros Hb.
+ destruct b as [|b|b]; discriminate Hb || clear Hb.
+ induction a; unfold pos_div_eucl; fold pos_div_eucl.
+ (* ~1 *)
+ destruct pos_div_eucl as (q,r).
+ simpl in IHa; destruct IHa as (Hr,Hr').
+ case gtb_spec; intros H; unfold snd. split; trivial. now destruct r.
+ split. unfold le.
+  now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
+ apply AUX. rewrite <- succ_double_spec.
+ destruct r; try easy. unfold lt in *; simpl in *.
+  now rewrite Pos.compare_xI_xO, Hr'.
+ (* ~0 *)
+ destruct pos_div_eucl as (q,r).
+ simpl in IHa; destruct IHa as (Hr,Hr').
+ case gtb_spec; intros H; unfold snd. split; trivial. now destruct r.
+ split. unfold le.
+  now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
+ apply AUX. destruct r; try easy.
+ (* 1 *)
+ case geb_spec; intros H; simpl; split; try easy.
+ red; simpl. now apply Pos.le_succ_l.
+Qed.
+
+Lemma mod_pos_bound a b : 0 < b -> 0 <= a mod b < b.
 Proof.
-  intros x y z; destruct x; destruct y; destruct z; simpl;
-    try rewrite Pmult_assoc; reflexivity.
+ destruct b as [|b|b]; try easy; intros _.
+ destruct a as [|a|a]; unfold modulo, div_eucl.
+ now split.
+ now apply pos_div_eucl_bound.
+ generalize (pos_div_eucl_bound a (Zpos b) (eq_refl _)).
+ destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
+ destruct r as [|r|r]; (now destruct Hr) || clear Hr.
+ now split.
+ split. unfold le.
+  now rewrite <- compare_antisym, <- compare_sub, compare_antisym, Hr'.
+ unfold lt in *; simpl in *. rewrite Pos.compare_antisym, Hr'.
+ simpl. now apply Pos.sub_decr.
 Qed.
 
-Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p).
+Definition mod_bound_pos a b (_:0<=a) := mod_pos_bound a b.
+
+Lemma mod_neg_bound a b : b < 0 -> b < a mod b <= 0.
 Proof.
-  intros n m p; rewrite Zmult_assoc; trivial with arith.
+ destruct b as [|b|b]; try easy; intros _.
+ destruct a as [|a|a]; unfold modulo, div_eucl.
+ now split.
+ generalize (pos_div_eucl_bound a (Zpos b) (eq_refl _)).
+ destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
+ destruct r as [|r|r]; (now destruct Hr) || clear Hr.
+ now split.
+ split.
+ unfold lt in *; simpl in *. rewrite Pos.compare_antisym, Hr'.
+ simpl. rewrite <- Pos.compare_antisym. now apply Pos.sub_decr.
+ change (Zneg b - Zneg r <= 0). unfold le, lt in *.
+  rewrite <- compare_sub. simpl in *.
+  now rewrite <- Pos.compare_antisym, Hr'.
+ generalize (pos_div_eucl_bound a (Zpos b) (eq_refl _)).
+ destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
+ split; destruct r; try easy.
+  red; simpl; now rewrite <- Pos.compare_antisym.
 Qed.
 
-(** ** Associativity mixed with commutativity *)
+(** ** Correctness proofs for Floor division *)
+
+Theorem quotrem_eq a b : let (q,r) := quotrem a b in a = q * b + r.
+Proof.
+ destruct a as [|a|a], b as [|b|b]; simpl; trivial;
+ generalize (N.pos_div_eucl_spec a (Npos b)); case N.pos_div_eucl; trivial;
+  intros q r; rewrite <- ?opp_Zpos;
+  change (Zpos a) with (of_N (Npos a)); intros ->; now destruct q, r.
+Qed.
 
-Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p).
+Lemma quot_rem' a b : a = b*(a÷b) + rem a b.
 Proof.
-  intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x).
-  apply Zmult_assoc.
+ rewrite mul_comm. generalize (quotrem_eq a b).
+ unfold quot, rem. now destruct quotrem.
 Qed.
 
-(** ** Z is integral *)
+Lemma quot_rem a b : b<>0 -> a = b*(a÷b) + rem a b.
+Proof. intros _. apply quot_rem'. Qed.
 
-Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0.
+Lemma rem_bound_pos a b : 0<=a -> 0<b -> 0 <= rem a b < b.
 Proof.
-  intros x y; destruct x as [| p| p].
-  intro H; absurd (Z0 = Z0); trivial.
-  intros _ H; destruct y as [| q| q]; reflexivity || discriminate.
-  intros _ H; destruct y as [| q| q]; reflexivity || discriminate.
+ intros Ha Hb.
+ destruct b as [|b|b]; (now discriminate Hb) || clear Hb;
+ destruct a as [|a|a]; (now destruct Ha) || clear Ha.
+ compute. now split.
+ unfold rem, quotrem.
+ assert (H := N.pos_div_eucl_remainder a (Npos b)).
+ destruct N.pos_div_eucl as (q,[|r]); simpl; split; try easy.
+ now apply H.
 Qed.
 
+Lemma rem_opp_l' a b : rem (-a) b = - (rem a b).
+Proof.
+ destruct a, b; trivial; unfold rem; simpl;
+  now destruct N.pos_div_eucl as (q,[|r]).
+Qed.
 
-Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0.
+Lemma rem_opp_r' a b : rem a (-b) = rem a b.
 Proof.
-  intros x y; destruct x; destruct y; auto; simpl; intro H;
-    discriminate H.
+ destruct a, b; trivial; unfold rem; simpl;
+  now destruct N.pos_div_eucl as (q,[|r]).
 Qed.
 
+Lemma rem_opp_l a b : b<>0 -> rem (-a) b = - (rem a b).
+Proof. intros _. apply rem_opp_l'. Qed.
+
+Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b.
+Proof. intros _. apply rem_opp_r'. Qed.
+
+(** ** Basic properties of divisibility *)
 
-Lemma Zmult_1_inversion_l :
-  forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1.
+Lemma divide_Zpos p q : (Zpos p|Zpos q) <-> (p|q)%positive.
 Proof.
-  intros x y; destruct x as [| p| p]; intro; [ discriminate | left | right ];
-    (destruct y as [| q| q]; try discriminate; simpl in H; injection H; clear H;
-      intro H; rewrite Pmult_1_inversion_l with (1 := H);
-	reflexivity).
+ split.
+ intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto.
+ intros (r,H). exists (Zpos r); simpl; now f_equal.
 Qed.
 
-(** ** Multiplication and Doubling *)
+Lemma divide_Zpos_Zneg_r n p : (n|Zpos p) <-> (n|Zneg p).
+Proof.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_r, H.
+Qed.
 
-Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z.
+Lemma divide_Zpos_Zneg_l n p : (Zpos p|n) <-> (Zneg p|n).
 Proof.
-  reflexivity.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_r, <- mul_opp_l.
 Qed.
 
-Lemma Zdouble_plus_one_mult : forall z,
-  Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1).
+(** ** Correctness proofs for gcd *)
+
+Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.
 Proof.
-  destruct z; simpl; auto with zarith.
+ destruct a as [ |p|p], b as [ |q|q]; simpl; auto;
+  generalize (Pos.ggcd_gcd p q); destruct Pos.ggcd as (g,(aa,bb));
+  simpl; congruence.
 Qed.
 
-(** ** Multiplication and Opposite *)
+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|p], b as [ |q|q]; simpl; rewrite ?Pos.mul_1_r; auto;
+  generalize (Pos.ggcd_correct_divisors p q);
+  destruct Pos.ggcd as (g,(aa,bb)); simpl; destruct 1; now subst.
+Qed.
 
-Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m.
+Lemma gcd_divide_l a b : (gcd a b | a).
 Proof.
-  intros x y; destruct x; destruct y; reflexivity.
+ rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
+ destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto.
 Qed.
 
-Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m.
+Lemma gcd_divide_r a b : (gcd a b | b).
 Proof.
-  intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l;
-    apply Zmult_comm.
+ rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
+ destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto.
 Qed.
 
-Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m).
+Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b).
 Proof.
-  intros x y; symmetry ; apply Zopp_mult_distr_l.
+ assert (H : forall p q r, (r|Zpos p) -> (r|Zpos q) -> (r|Zpos (Pos.gcd p q))).
+  intros p q [|r|r] H H'.
+  now destruct H.
+  apply divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos.
+  apply divide_Zpos_Zneg_l, divide_Zpos, Pos.gcd_greatest;
+   now apply divide_Zpos, divide_Zpos_Zneg_l.
+ destruct a, b; simpl; auto; intros; try apply H; trivial;
+  now apply divide_Zpos_Zneg_r.
 Qed.
 
-Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m.
+Lemma gcd_nonneg a b : 0 <= gcd a b.
 Proof.
-  intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r;
-    trivial with arith.
+ now destruct a, b.
 Qed.
 
-Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m.
+(** ggcd and opp : an auxiliary result used in QArith *)
+
+Theorem ggcd_opp a b :
+  ggcd (-a) b = (let '(g,(aa,bb)) := ggcd a b in (g,(-aa,bb))).
 Proof.
-  intros x y; destruct x; destruct y; reflexivity.
+ destruct a as [|a|a], b as [|b|b]; unfold ggcd, opp; auto;
+  destruct (Pos.ggcd a b) as (g,(aa,bb)); auto.
 Qed.
 
-Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1.
+(** ** Conversions between [Z.testbit] and [N.testbit] *)
+
+Lemma testbit_of_N a n :
+ testbit (of_N a) (of_N n) = N.testbit a n.
 Proof.
-  intro x; induction x; intros; rewrite Zmult_comm; auto with arith.
+ destruct a as [|a], n; simpl; trivial. now destruct a.
 Qed.
 
-(** ** Distributivity of multiplication over addition *)
+Lemma testbit_of_N' a n : 0<=n ->
+ testbit (of_N a) n = N.testbit a (to_N n).
+Proof.
+ intro Hn. rewrite <- testbit_of_N. f_equal.
+ destruct n; trivial; now destruct Hn.
+Qed.
 
-Lemma weak_Zmult_plus_distr_r :
-  forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m.
+Lemma testbit_Zpos a n : 0<=n ->
+ testbit (Zpos a) n = N.testbit (Npos a) (to_N n).
 Proof.
- intros x [ |y|y] [ |z|z]; simpl; trivial; f_equal;
-  apply Pmult_plus_distr_l || rewrite Pmult_compare_mono_l;
-  case_eq ((y ?= z)%positive); intros H; trivial;
-   rewrite Pmult_minus_distr_l; trivial; now apply ZC1.
+ intro Hn. now rewrite <- testbit_of_N'.
 Qed.
 
-Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p.
+Lemma testbit_Zneg a n : 0<=n ->
+ testbit (Zneg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)).
 Proof.
- intros [|x|x] y z. trivial.
- apply weak_Zmult_plus_distr_r.
- apply Zopp_inj; rewrite Zopp_plus_distr, !Zopp_mult_distr_l, !Zopp_neg.
- apply weak_Zmult_plus_distr_r.
+ intro Hn.
+ rewrite <- testbit_of_N' by trivial.
+ destruct n as [ |n|n];
+  [ | simpl; now destruct (Ppred_N a) | now destruct Hn].
+ unfold testbit.
+ now destruct a as [|[ | | ]| ].
 Qed.
 
-Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p.
+(** ** Proofs of specifications for bitwise operations *)
+
+Lemma div2_spec a : div2 a = shiftr a 1.
 Proof.
-  intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r;
-    do 2 rewrite (Zmult_comm p); trivial with arith.
+ reflexivity.
 Qed.
 
-(** ** Distributivity of multiplication over subtraction *)
+Lemma testbit_0_l n : testbit 0 n = false.
+Proof.
+ now destruct n.
+Qed.
 
-Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p.
+Lemma testbit_neg_r a n : n<0 -> testbit a n = false.
 Proof.
-  intros x y z; unfold Zminus.
-  rewrite <- Zopp_mult_distr_l_reverse.
-  apply Zmult_plus_distr_l.
+ now destruct n.
 Qed.
 
+Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
+Proof.
+ now destruct a as [|a|[a|a|]].
+Qed.
 
-Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m.
+Lemma testbit_even_0 a : testbit (2*a) 0 = false.
 Proof.
-  intros x y z; rewrite (Zmult_comm z (x - y)).
-  rewrite (Zmult_comm z x).
-  rewrite (Zmult_comm z y).
-  apply Zmult_minus_distr_r.
+ now destruct a.
 Qed.
 
-(** ** Simplification of multiplication for non-zero integers *)
+Lemma testbit_odd_succ a n : 0<=n ->
+ testbit (2*a+1) (succ n) = testbit a n.
+Proof.
+ destruct n as [|n|n]; (now destruct 1) || intros _.
+ destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a.
+ unfold testbit. rewrite succ_Zpos.
+ destruct a as [|a|[a|a|]]; simpl; trivial;
+  rewrite ?Pos.pred_N_succ; now destruct n.
+Qed.
 
-Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m.
+Lemma testbit_even_succ a n : 0<=n ->
+ testbit (2*a) (succ n) = testbit a n.
 Proof.
-  intros x y z H H0.
-  generalize (Zeq_minus _ _ H0).
-  intro.
-  apply Zminus_eq.
-  rewrite <- Zmult_minus_distr_l in H1.
-  clear H0; destruct (Zmult_integral _ _ H1).
-  contradiction.
-  trivial.
+ destruct n as [|n|n]; (now destruct 1) || intros _.
+ destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a.
+ unfold testbit. rewrite succ_Zpos.
+ destruct a as [|a|[a|a|]]; simpl; trivial;
+  rewrite ?Pos.pred_N_succ; now destruct n.
 Qed.
 
-Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m.
+Lemma div2_of_N n : of_N (N.div2 n) = div2 (of_N n).
+Proof.
+ now destruct n as [|[ | | ]].
+Qed.
+
+(** Correctness proofs about [Zshiftr] and [Zshiftl] *)
+
+Lemma shiftr_spec_aux a n m : 0<=n -> 0<=m ->
+ testbit (shiftr a n) m = testbit a (m+n).
 Proof.
-  intros x y z Hz.
-  rewrite (Zmult_comm x z).
-  rewrite (Zmult_comm y z).
-  intro; apply Zmult_reg_l with z; assumption.
+ intros Hn Hm. unfold shiftr.
+ destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl.
+ now rewrite add_0_r.
+ assert (forall p, to_N (m + Zpos p) = (to_N m + Npos p)%N).
+  destruct m; trivial; now destruct Hm.
+ assert (forall p, 0 <= m + Zpos p).
+  destruct m; easy || now destruct Hm.
+ destruct a as [ |a|a].
+ (* a = 0 *)
+ replace (Pos.iter n div2 0) with 0
+  by (apply Pos.iter_invariant; intros; subst; trivial).
+ now rewrite 2 testbit_0_l.
+ (* a > 0 *)
+ change (Zpos a) with (of_N (Npos a)) at 1.
+ rewrite <- (Pos.iter_swap_gen _ _ _ Ndiv2) by exact div2_of_N.
+ rewrite testbit_Zpos, testbit_of_N', H; trivial.
+ exact (N.shiftr_spec' (Npos a) (Npos n) (to_N m)).
+ (* a < 0 *)
+ rewrite <- (Pos.iter_swap_gen _ _ _ Pdiv2_up) by trivial.
+ rewrite 2 testbit_Zneg, H; trivial. f_equal.
+ rewrite (Pos.iter_swap_gen _ _ _ _ Ndiv2) by exact N.pred_div2_up.
+ exact (N.shiftr_spec' (Ppred_N a) (Npos n) (to_N m)).
 Qed.
 
-(** ** Addition and multiplication by 2 *)
+Lemma shiftl_spec_low a n m : m<n ->
+ testbit (shiftl a n) m = false.
+Proof.
+ intros H. destruct n as [|n|n], m as [|m|m]; try easy; simpl shiftl.
+ destruct (Pos.succ_pred_or n) as [-> | <-];
+  rewrite ?Pos.iter_succ; apply testbit_even_0.
+ destruct a as [ |a|a].
+ (* a = 0 *)
+ replace (Pos.iter n (mul 2) 0) with 0
+  by (apply Pos.iter_invariant; intros; subst; trivial).
+ apply testbit_0_l.
+ (* a > 0 *)
+ rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial.
+ rewrite testbit_Zpos by easy.
+ exact (N.shiftl_spec_low (Npos a) (Npos n) (Npos m) H).
+ (* a < 0 *)
+ rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial.
+ rewrite testbit_Zneg by easy.
+ now rewrite (N.pos_pred_shiftl_low a (Npos n)).
+Qed.
 
-Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2.
+Lemma shiftl_spec_high a n m : 0<=m -> n<=m ->
+ testbit (shiftl a n) m = testbit a (m-n).
 Proof.
-  intros x; pattern x at 1 2; rewrite <- (Zmult_1_r x);
-    rewrite <- Zmult_plus_distr_r; reflexivity.
+ intros Hm H.
+ destruct n as [ |n|n]. simpl. now rewrite sub_0_r.
+ (* n > 0 *)
+ destruct m as [ |m|m]; try (now destruct H).
+ assert (0 <= Zpos m - Zpos n).
+  red. now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
+ assert (EQ : to_N (Zpos m - Zpos n) = (Npos m - Npos n)%N).
+  red in H. simpl in H. simpl to_N.
+  rewrite Pos.compare_antisym.
+  destruct (Pos.compare_spec n m) as [H'|H'|H']; try (now destruct H).
+  subst. now rewrite N.sub_diag.
+  simpl. destruct (Pos.sub_mask_pos' m n H') as (p & -> & <-).
+  f_equal. now rewrite Pos.add_comm, Pos.add_sub.
+ destruct a; unfold shiftl.
+ (* ... a = 0 *)
+ replace (Pos.iter n (mul 2) 0) with 0
+  by (apply Pos.iter_invariant; intros; subst; trivial).
+ now rewrite 2 testbit_0_l.
+ (* ... a > 0 *)
+ rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial.
+ rewrite 2 testbit_Zpos, EQ by easy.
+ exact (N.shiftl_spec_high' (Npos p) (Npos n) (Npos m) H).
+ (* ... a < 0 *)
+ rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial.
+ rewrite 2 testbit_Zneg, EQ by easy. f_equal.
+ simpl to_N.
+ rewrite <- N.shiftl_spec_high by easy.
+ now apply (N.pos_pred_shiftl_high p (Npos n)).
+ (* n < 0 *)
+ unfold sub. simpl.
+ now apply (shiftr_spec_aux a (Zpos n) m).
+Qed.
+
+Lemma shiftr_spec a n m : 0<=m ->
+ testbit (shiftr a n) m = testbit a (m+n).
+Proof.
+ intros Hm.
+ destruct (leb_spec 0 n).
+ now apply shiftr_spec_aux.
+ destruct (leb_spec (-n) m) as [LE|GT].
+ unfold shiftr.
+ rewrite (shiftl_spec_high a (-n) m); trivial. now destruct n.
+ unfold shiftr.
+ rewrite (shiftl_spec_low a (-n) m); trivial.
+ rewrite testbit_neg_r; trivial.
+ red in GT. rewrite compare_sub in GT. now destruct n.
 Qed.
 
-(** ** Multiplication and successor *)
+(** Correctness proofs for bitwise operations *)
 
-Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n.
+Lemma lor_spec a b n :
+ testbit (lor a b) n = testbit a n || testbit b n.
 Proof.
-  intros n m; unfold Zsucc; rewrite Zmult_plus_distr_r;
-    rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l;
-      trivial with arith.
+ destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?testbit_0_l, ?orb_false_r; trivial; unfold lor;
+  rewrite ?testbit_Zpos, ?testbit_Zneg, ?N.pos_pred_succ by trivial.
+ now rewrite <- N.lor_spec.
+ now rewrite N.ldiff_spec, negb_andb, negb_involutive, orb_comm.
+ now rewrite N.ldiff_spec, negb_andb, negb_involutive.
+ now rewrite N.land_spec, negb_andb.
 Qed.
 
-Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m.
+Lemma land_spec a b n :
+ testbit (land a b) n = testbit a n && testbit b n.
 Proof.
-  intros; symmetry ; apply Zmult_succ_r.
+ destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?testbit_0_l, ?andb_false_r; trivial; unfold land;
+  rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ
+   by trivial.
+ now rewrite <- N.land_spec.
+ now rewrite N.ldiff_spec.
+ now rewrite N.ldiff_spec, andb_comm.
+ now rewrite N.lor_spec, negb_orb.
 Qed.
 
-Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m.
+Lemma ldiff_spec a b n :
+ testbit (ldiff a b) n = testbit a n && negb (testbit b n).
 Proof.
-  intros n m; unfold Zsucc; rewrite Zmult_plus_distr_l;
-    rewrite Zmult_1_l; trivial with arith.
+ destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?testbit_0_l, ?andb_true_r; trivial; unfold ldiff;
+  rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ
+   by trivial.
+ now rewrite <- N.ldiff_spec.
+ now rewrite N.land_spec, negb_involutive.
+ now rewrite N.lor_spec, negb_orb.
+ now rewrite N.ldiff_spec, negb_involutive, andb_comm.
 Qed.
 
-Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m.
+Lemma lxor_spec a b n :
+ testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
+Proof.
+ destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r].
+ destruct a as [ |a|a], b as [ |b|b];
+  rewrite ?testbit_0_l, ?xorb_false_l, ?xorb_false_r; trivial; unfold lxor;
+  rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ
+   by trivial.
+ now rewrite <- N.lxor_spec.
+ now rewrite N.lxor_spec, negb_xorb_r.
+ now rewrite N.lxor_spec, negb_xorb_l.
+ now rewrite N.lxor_spec, xorb_negb_negb.
+Qed.
+
+(** An additionnal proof concerning [Pos.shiftl_nat], used in BigN *)
+
+Lemma pos_shiftl_nat_pow n p :
+  Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
 Proof.
-  intros; symmetry; apply Zmult_succ_l.
+ intros.
+ rewrite mul_comm.
+ induction n. simpl; auto.
+ transitivity (2 * (2 ^ Z.of_nat n * Zpos p)).
+ rewrite <- IHn. auto.
+ rewrite mul_assoc.
+ replace (of_nat (S n)) with (succ (of_nat n)).
+ rewrite <- pow_succ_r. trivial.
+ now destruct n.
+ destruct n. trivial. simpl. now rewrite Pos.add_1_r.
 Qed.
 
+(** ** Properties of [succ'] and [pred'] *)
 
+Lemma succ'_pred' n : succ' (pred' n) = n.
+Proof.
+ rewrite <- succ_succ', <- pred_pred'. apply succ_pred.
+Qed.
 
-(** ** Misc redundant properties *)
+Lemma pred'_succ' n : pred' (succ' n) = n.
+Proof.
+ rewrite <- succ_succ', <- pred_pred'. apply pred_succ.
+Qed.
 
-Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0.
+Lemma succ'_inj n m : succ' n = succ' m -> n = m.
 Proof.
-  intros x y H; rewrite H; auto with arith.
+ intros H. now rewrite <- (pred'_succ' n), <- (pred'_succ' m), H.
 Qed.
 
+Lemma pred'_inj n m : pred' n = pred' m -> n = m.
+Proof.
+ intros H. now rewrite <- (succ'_pred' n), <- (succ'_pred' m), H.
+Qed.
 
+Lemma neq_succ'_diag_r n : n <> succ' n.
+Proof.
+ rewrite <- succ_succ'. rewrite <- compare_eq_iff.
+ rewrite compare_sub, sub_succ_r. unfold sub. now rewrite add_opp_diag_r.
+Qed.
 
-(**********************************************************************)
-(** * Relating binary positive numbers and binary integers *)
+(** ** Induction principles based on successor / predecessor *)
 
-Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q.
+Lemma peano_ind (P : Z -> Prop) :
+  P 0 ->
+  (forall x, P x -> P (succ' x)) ->
+  (forall x, P x -> P (pred' x)) ->
+  forall z, P z.
 Proof.
-  intros; f_equal; auto.
+ intros H0 Hs Hp z; destruct z.
+ assumption.
+ induction p using Pos.peano_ind.
+  now apply (Hs 0).
+  now apply (Hs (Zpos p)).
+ induction p using Pos.peano_ind.
+  now apply (Hp 0).
+  now apply (Hp (Zneg p)).
 Qed.
 
-Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q.
+Lemma bi_induction (P : Z -> Prop) :
+  Proper (eq ==> iff) P ->
+  P 0 ->
+  (forall x, P x <-> P (succ x)) ->
+  forall z, P z.
 Proof.
-  inversion 1; auto.
+ intros _ H0 Hs. induction z using peano_ind.
+ assumption.
+ rewrite <- succ_succ'. now apply -> Hs.
+ rewrite <- pred_pred'. apply Hs. now rewrite succ_pred.
 Qed.
 
-Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q.
+
+(** * Proofs of morphisms, obvious since eq is Leibniz *)
+
+Local Obligation Tactic := simpl_relation.
+Program Definition succ_wd : Proper (eq==>eq) succ := _.
+Program Definition pred_wd : Proper (eq==>eq) pred := _.
+Program Definition opp_wd : Proper (eq==>eq) opp := _.
+Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
+Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
+Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
+Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
+Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
+Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
+Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
+Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
+Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
+Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+
+Set Inline Level 30. (* For inlining only t eq zero one two *)
+
+Include ZProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+
+(** Otherwise Z stays associated with abstract_scope : (TODO FIX) *)
+Bind Scope Z_scope with Z.
+
+(** TODO : to add in Numbers *)
+
+Lemma add_shuffle3 n m p : n + (m + p) = m + (n + p).
 Proof.
-  split; [apply Zpos_eq|apply Zpos_eq_rev].
+ now rewrite add_comm, <- add_assoc, (add_comm p).
 Qed.
 
-Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1.
+Lemma mul_shuffle3 n m p : n * (m * p) = m * (n * p).
 Proof.
-  intro; apply refl_equal.
+ now rewrite mul_assoc, (mul_comm n), mul_assoc.
 Qed.
 
-Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p.
+Lemma add_reg_l n m p : n + m = n + p -> m = p.
 Proof.
-  intro; apply refl_equal.
+ exact (proj1 (add_cancel_l m p n)).
 Qed.
 
-Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1.
+Lemma mul_reg_l n m p : p <> 0 -> p * n = p * m -> n = m.
 Proof.
-  intro; apply refl_equal.
+ exact (fun Hp => proj1 (mul_cancel_l n m p Hp)).
 Qed.
 
-Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p.
+Lemma mul_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
 Proof.
-  reflexivity.
+ exact (fun Hp => proj1 (mul_cancel_r n m p Hp)).
 Qed.
 
-Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q.
+Lemma add_succ_comm n m : succ n + m = n + succ m.
 Proof.
-  intros p p'; destruct p;
-    [ destruct p' as [p0| p0| ]
-      | destruct p' as [p0| p0| ]
-      | destruct p' as [p| p| ] ]; reflexivity.
+ now rewrite add_succ_r, add_succ_l.
 Qed.
 
-Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q.
+Lemma mul_opp_comm n m : - n * m = n * - m.
 Proof.
-  intros p p'; destruct p;
-    [ destruct p' as [p0| p0| ]
-      | destruct p' as [p0| p0| ]
-      | destruct p' as [p| p| ] ]; reflexivity.
+ now destruct n, m.
 Qed.
 
-(**********************************************************************)
-(** * Order relations *)
+Notation mul_eq_0 := eq_mul_0.
 
-Definition Zlt (x y:Z) := (x ?= y) = Lt.
-Definition Zgt (x y:Z) := (x ?= y) = Gt.
-Definition Zle (x y:Z) := (x ?= y) <> Gt.
-Definition Zge (x y:Z) := (x ?= y) <> Lt.
-Definition Zne (x y:Z) := x <> y.
+Lemma mul_eq_0_l n m : n <> 0 -> m * n = 0 -> m = 0.
+Proof.
+ intros Hn H. apply eq_mul_0 in H. now destruct H.
+Qed.
 
-Infix "<=" := Zle : Z_scope.
-Infix "<" := Zlt : Z_scope.
-Infix ">=" := Zge : Z_scope.
-Infix ">" := Zgt : Z_scope.
+Notation mul_eq_1 := eq_mul_1.
 
-Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
-Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
-Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
-Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
+Lemma opp_eq_mul_m1 n : - n = n * -1.
+Proof.
+ rewrite mul_comm. now destruct n.
+Qed.
 
-Lemma Zpos_lt : forall p q, Zlt (Zpos p) (Zpos q) <-> Plt p q.
+Lemma add_diag n : n + n = 2 * n.
 Proof.
- intros. apply iff_refl.
+ change 2 with (1+1). now rewrite mul_add_distr_r, !mul_1_l.
 Qed.
 
-Lemma Zpos_le : forall p q, Zle (Zpos p) (Zpos q) <-> Ple p q.
+(** * Comparison and opposite *)
+
+Lemma compare_opp n m : (- n ?= - m) = (m ?= n).
 Proof.
- intros. apply iff_refl.
+ destruct n, m; simpl; trivial; intros; now rewrite <- Pos.compare_antisym.
 Qed.
 
-(**********************************************************************)
-(** * Minimum and maximum *)
+(** * Comparison and addition *)
 
-Definition Zmax (n m:Z) :=
-  match n ?= m with
-    | Eq | Gt => n
-    | Lt => m
-  end.
+Lemma add_compare_mono_l n m p : (n + m ?= n + p) = (m ?= p).
+Proof.
+ rewrite (compare_sub m p), compare_sub. f_equal.
+ unfold sub. rewrite opp_add_distr, (add_comm n m), add_assoc.
+ f_equal. now rewrite <- add_assoc, add_opp_diag_r, add_0_r.
+Qed.
 
-Definition Zmin (n m:Z) :=
-  match n ?= m with
-    | Eq | Lt => n
-    | Gt => m
-  end.
+End Z.
 
-(**********************************************************************)
-(** * Absolute value on integers *)
+(** Export Notations *)
 
-Definition Zabs_nat (x:Z) : nat :=
-  match x with
-    | Z0 => 0%nat
-    | Zpos p => nat_of_P p
-    | Zneg p => nat_of_P p
-  end.
+Infix "+" := Z.add : Z_scope.
+Notation "- x" := (Z.opp x) : Z_scope.
+Infix "-" := Z.sub : Z_scope.
+Infix "*" := Z.mul : Z_scope.
+Infix "^" := Z.pow : Z_scope.
+Infix "/" := Z.div : Z_scope.
+Infix "mod" := Z.modulo (at level 40, no associativity) : Z_scope.
+Infix "÷" := Z.quot (at level 40, left associativity) : Z_scope.
 
-Definition Zabs (z:Z) : Z :=
-  match z with
-    | Z0 => Z0
-    | Zpos p => Zpos p
-    | Zneg p => Zpos p
-  end.
+(* TODO : transition from Zdivide *)
+Notation "( x | y )" := (Z.divide x y) (at level 0).
 
-(**********************************************************************)
-(** * From [nat] to [Z] *)
+Infix "?=" := Z.compare (at level 70, no associativity) : Z_scope.
 
-Definition Z_of_nat (x:nat) :=
-  match x with
-    | O => Z0
-    | S y => Zpos (P_of_succ_nat y)
-  end.
+Infix "<=" := Z.le : Z_scope.
+Infix "<" := Z.lt : Z_scope.
+Infix ">=" := Z.ge : Z_scope.
+Infix ">" := Z.gt : Z_scope.
 
-Definition Zabs_N (z:Z) :=
-  match z with
-    | Z0 => 0%N
-    | Zpos p => Npos p
-    | Zneg p => Npos p
-  end.
+Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
+Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
 
-Definition Z_of_N (x:N) :=
-  match x with
-    | N0 => Z0
-    | Npos p => Zpos p
-  end.
+Infix "=?" := Z.eqb (at level 70, no associativity) : Z_scope.
+Infix "<=?" := Z.leb (at level 70, no associativity) : Z_scope.
+Infix "<?" := Z.ltb (at level 70, no associativity) : Z_scope.
+Infix ">=?" := Z.geb (at level 70, no associativity) : Z_scope.
+Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope.
 
 (** Compatibility Notations *)
 
+Notation Zdouble_plus_one := Z.succ_double (only parsing).
+Notation Zdouble_minus_one := Z.pred_double (only parsing).
+Notation Zdouble := Z.double (only parsing).
+Notation ZPminus := Z.pos_sub (only parsing).
+Notation Zplus := Z.add (only parsing).
+Notation Zopp := Z.opp (only parsing).
+Notation Zsucc := Z.succ (only parsing).
+Notation Zpred := Z.pred (only parsing).
+Notation Zminus := Z.sub (only parsing).
+Notation Zmult := Z.mul (only parsing).
+Notation Zcompare := Z.compare (only parsing).
+Notation Zsgn := Z.sgn (only parsing).
+Notation Zsucc' := Z.succ' (only parsing).
+Notation Zpred' := Z.pred' (only parsing).
+Notation Zplus' := Z.add' (only parsing).
+Notation Zle := Z.le (only parsing).
+Notation Zge := Z.ge (only parsing).
+Notation Zlt := Z.lt (only parsing).
+Notation Zgt := Z.gt (only parsing).
+Notation Zmax := Z.max (only parsing).
+Notation Zmin := Z.min (only parsing).
+Notation Zabs := Z.abs (only parsing).
+Notation Zabs_nat := Z.abs_nat (only parsing).
+Notation Zabs_N := Z.abs_N (only parsing).
+Notation Z_of_nat := Z.of_nat (only parsing).
+Notation Z_of_N := Z.of_N (only parsing).
+
+Notation Zind := Z.peano_ind (only parsing).
+Notation Zopp_0 := Z.opp_0 (only parsing).
+Notation Zopp_neg := Z.opp_Zneg (only parsing).
+Notation Zopp_involutive := Z.opp_involutive (only parsing).
+Notation Zopp_inj := Z.opp_inj (only parsing).
+Notation Zplus_0_l := Z.add_0_l (only parsing).
+Notation Zplus_0_r := Z.add_0_r (only parsing).
+Notation Zplus_comm := Z.add_comm (only parsing).
+Notation Zopp_plus_distr := Z.opp_add_distr (only parsing).
+Notation Zopp_succ := Z.opp_succ (only parsing).
+Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing).
+Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing).
+Notation Zplus_assoc := Z.add_assoc (only parsing).
+Notation Zplus_permute := Z.add_shuffle3 (only parsing).
+Notation Zplus_reg_l := Z.add_reg_l (only parsing).
+Notation Zplus_succ_l := Z.add_succ_l (only parsing).
+Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
+Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
+Notation Zsucc_inj := Z.succ_inj (only parsing).
+Notation Zsucc_succ' := Z.succ_succ' (only parsing).
+Notation Zpred_pred' := Z.pred_pred' (only parsing).
+Notation Zsucc'_inj := Z.succ'_inj (only parsing).
+Notation Zsucc'_pred' := Z.succ'_pred' (only parsing).
+Notation Zpred'_succ' := Z.pred'_succ' (only parsing).
+Notation Zpred'_inj := Z.pred'_inj (only parsing).
+Notation Zsucc'_discr := Z.neq_succ'_diag_r (only parsing).
+Notation Zminus_0_r := Z.sub_0_r (only parsing).
+Notation Zminus_diag := Z.sub_diag (only parsing).
+Notation Zminus_plus_distr := Z.sub_add_distr (only parsing).
+Notation Zminus_succ_r := Z.sub_succ_r (only parsing).
+Notation Zminus_plus := Z.add_simpl_l (only parsing).
+Notation Zmult_0_l := Z.mul_0_l (only parsing).
+Notation Zmult_0_r := Z.mul_0_r (only parsing).
+Notation Zmult_1_l := Z.mul_1_l (only parsing).
+Notation Zmult_1_r := Z.mul_1_r (only parsing).
+Notation Zmult_comm := Z.mul_comm (only parsing).
+Notation Zmult_assoc := Z.mul_assoc (only parsing).
+Notation Zmult_permute := Z.mul_shuffle3 (only parsing).
+Notation Zmult_integral_l := Z.mul_eq_0_l (only parsing).
+Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing).
+Notation Zdouble_mult := Z.double_spec (only parsing).
+Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing).
+Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing).
+Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing).
+Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing).
+Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing).
+Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing).
+Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing).
+Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing).
+Notation Zmult_reg_l := Z.mul_reg_l (only parsing).
+Notation Zmult_reg_r := Z.mul_reg_r (only parsing).
+Notation Zmult_succ_l := Z.mul_succ_l (only parsing).
+Notation Zmult_succ_r := Z.mul_succ_r (only parsing).
+Notation Zpos_xI := Z.pos_xI (only parsing).
+Notation Zpos_xO := Z.pos_xO (only parsing).
+Notation Zneg_xI := Z.neg_xI (only parsing).
+Notation Zneg_xO := Z.neg_xO (only parsing).
+
 Notation Z := Z (only parsing).
 Notation Z_rect := Z_rect (only parsing).
 Notation Z_rec := Z_rec (only parsing).
@@ -1046,3 +1491,118 @@ Notation Z_ind := Z_ind (only parsing).
 Notation Z0 := Z0 (only parsing).
 Notation Zpos := Zpos (only parsing).
 Notation Zneg := Zneg (only parsing).
+
+(** Compatibility lemmas. These could be notations,
+    but scope information would be lost.
+*)
+
+Notation SYM1 lem := (fun n => eq_sym (lem n)).
+Notation SYM2 lem := (fun n m => eq_sym (lem n m)).
+Notation SYM3 lem := (fun n m p => eq_sym (lem n m p)).
+
+Lemma Zplus_assoc_reverse : forall n m p, n+m+p = n+(m+p).
+Proof (SYM3 Z.add_assoc).
+Lemma Zplus_succ_r_reverse : forall n m, Z.succ (n+m) = n+Z.succ m.
+Proof (SYM2 Z.add_succ_r).
+Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
+Lemma Zplus_0_r_reverse : forall n, n = n + 0.
+Proof (SYM1 Z.add_0_r).
+Lemma Zplus_eq_compat : forall n m p q, n=m -> p=q -> n+p=m+q.
+Proof (f_equal2 Z.add).
+Lemma Zpos_succ_morphism : forall p, Zpos (Psucc p) = Zsucc (Zpos p).
+Proof (SYM1 Z.succ_Zpos).
+Lemma Zsucc_pred : forall n, n = Z.succ (Z.pred n).
+Proof (SYM1 Z.succ_pred).
+Lemma Zpred_succ : forall n, n = Z.pred (Z.succ n).
+Proof (SYM1 Z.pred_succ).
+Lemma Zsucc_eq_compat : forall n m, n = m -> Z.succ n = Z.succ m.
+Proof (f_equal Z.succ).
+Lemma Zminus_0_l_reverse : forall n, n = n - 0.
+Proof (SYM1 Z.sub_0_r).
+Lemma Zminus_diag_reverse : forall n, 0 = n-n.
+Proof (SYM1 Z.sub_diag).
+Lemma Zminus_succ_l : forall n m, Z.succ (n - m) = Z.succ n - m.
+Proof (SYM2 Z.sub_succ_l).
+Lemma Zplus_minus_eq : forall n m p, n = m + p -> p = n - m.
+Proof. intros. now apply Z.add_move_l. Qed.
+Lemma Zplus_minus : forall n m, n + (m - n) = m.
+Proof (fun n m => eq_trans (Z.add_comm n (m-n)) (Z.sub_add n m)).
+Lemma Zminus_plus_simpl_l : forall n m p, p + n - (p + m) = n - m.
+Proof (fun n m p => Z.add_add_simpl_l_l p n m).
+Lemma Zminus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
+Proof (SYM3 Zminus_plus_simpl_l).
+Lemma Zminus_plus_simpl_r : forall n m p, n + p - (m + p) = n - m.
+Proof (fun n m p => Z.add_add_simpl_r_r n p m).
+Lemma Zpos_minus_morphism : forall a b,
+ Pcompare a b Eq = Lt -> Zpos (b - a) = Zpos b - Zpos a.
+Proof. intros. now rewrite Z.sub_Zpos. Qed.
+Lemma Zeq_minus : forall n m, n = m -> n - m = 0.
+Proof (fun n m => proj2 (Z.sub_move_0_r n m)).
+Lemma Zminus_eq : forall n m, n - m = 0 -> n = m.
+Proof (fun n m => proj1 (Z.sub_move_0_r n m)).
+Lemma Zpos_mult_morphism : forall p q, Zpos (p * q) = Zpos p * Zpos q.
+Proof (SYM2 Z.mul_Zpos).
+Lemma Zmult_0_r_reverse : forall n, 0 = n * 0.
+Proof (SYM1 Z.mul_0_r).
+Lemma Zmult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
+Proof (SYM3 Z.mul_assoc).
+Lemma Zmult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+Proof (fun n m => proj1 (Z.mul_eq_0 n m)).
+Lemma Zopp_mult_distr_l : forall n m, - (n * m) = - n * m.
+Proof (SYM2 Z.mul_opp_l).
+Lemma Zopp_mult_distr_r : forall n m, - (n * m) = n * - m.
+Proof (SYM2 Z.mul_opp_r).
+Lemma Zmult_minus_distr_l : forall n m p, p * (n - m) = p * n - p * m.
+Proof (fun n m p => Z.mul_sub_distr_l p n m).
+Lemma Zmult_succ_r_reverse : forall n m, n * m + n = n * Zsucc m.
+Proof (SYM2 Z.mul_succ_r).
+Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Zsucc n * m.
+Proof (SYM2 Z.mul_succ_l).
+Lemma Zpos_eq : forall p q, p = q -> Zpos p = Zpos q.
+Proof (fun p q => proj2 (Z.inj_Zpos p q)).
+Lemma Zpos_eq_rev : forall p q, Zpos p = Zpos q -> p = q.
+Proof (fun p q => proj1 (Z.inj_Zpos p q)).
+Lemma Zpos_eq_iff : forall p q, p = q <-> Zpos p = Zpos q.
+Proof (fun p q => iff_sym (Z.inj_Zpos p q)).
+Lemma Zpos_plus_distr : forall p q, Zpos (p + q) = Zpos p + Zpos q.
+Proof (SYM2 Z.add_Zpos).
+Lemma Zneg_plus_distr : forall p q, Zneg (p + q) = Zneg p + Zneg q.
+Proof (SYM2 Z.add_Zneg).
+
+Hint Immediate Zsucc_pred: zarith.
+
+(* Not kept :
+Zplus_0_simpl_l
+Zplus_0_simpl_l_reverse
+Zplus_opp_expand
+Zsucc_inj_contrapositive
+*)
+
+(* No compat notation for :
+weak_assoc (now Z.add_assoc_pos)
+weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos)
+*)
+
+(** Obsolete stuff *)
+
+Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *)
+
+Ltac elim_compare com1 com2 :=
+  case (Dcompare (com1 ?= com2)%Z);
+    [ idtac | let x := fresh "H" in
+      (intro x; case x; clear x) ].
+
+Lemma ZL0 : 2%nat = (1 + 1)%nat.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma Zplus_diag_eq_mult_2 n : n + n = n * 2.
+Proof.
+ rewrite Z.mul_comm. apply Z.add_diag.
+Qed.
+
+Lemma Z_eq_mult n m : m = 0 -> m * n = 0.
+Proof.
+ intros; now subst.
+Qed.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
new file mode 100644
index 000000000..b0fef2a9d
--- /dev/null
+++ b/theories/ZArith/BinIntDef.v
@@ -0,0 +1,634 @@
+(* -*- 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 Export BinNums.
+Require Import BinPos BinNat.
+
+Local Open Scope Z_scope.
+
+(***********************************************************)
+(** * Binary Integers, Definitions of Operations *)
+(***********************************************************)
+
+(** Initial author: Pierre Crégut, CNET, Lannion, France *)
+
+Module Z.
+
+Definition t := Z.
+
+(** ** Constants *)
+
+Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
+
+(** ** Doubling and variants *)
+
+Definition double x :=
+  match x with
+    | 0 => 0
+    | Zpos p => Zpos p~0
+    | Zneg p => Zneg p~0
+  end.
+
+Definition succ_double x :=
+  match x with
+    | 0 => 1
+    | Zpos p => Zpos p~1
+    | Zneg p => Zneg (Pos.pred_double p)
+  end.
+
+Definition pred_double x :=
+  match x with
+    | 0 => -1
+    | Zneg p => Zneg p~1
+    | Zpos p => Zpos (Pos.pred_double p)
+  end.
+
+(** ** Addition *)
+
+Definition add x y :=
+  match x, y with
+    | 0, y => y
+    | Zpos x', 0 => Zpos x'
+    | Zneg x', 0 => Zneg x'
+    | Zpos x', Zpos y' => Zpos (x' + y')
+    | Zpos x', Zneg y' =>
+      match (x' ?= y')%positive with
+	| Eq => 0
+	| Lt => Zneg (y' - x')
+	| Gt => Zpos (x' - y')
+      end
+    | Zneg x', Zpos y' =>
+      match (x' ?= y')%positive with
+	| Eq => 0
+	| Lt => Zpos (y' - x')
+	| Gt => Zneg (x' - y')
+      end
+    | Zneg x', Zneg y' => Zneg (x' + y')
+  end.
+
+Infix "+" := add : Z_scope.
+
+(** ** Opposite *)
+
+Definition opp x :=
+  match x with
+    | 0 => 0
+    | Zpos x => Zneg x
+    | Zneg x => Zpos x
+  end.
+
+Notation "- x" := (opp x) : Z_scope.
+
+(** ** Successor *)
+
+Definition succ x := x + 1.
+
+(** ** Predecessor *)
+
+Definition pred x := x + -1.
+
+(** ** Subtraction *)
+
+Definition sub m n := m + -n.
+
+Infix "-" := sub : Z_scope.
+
+(** ** Multiplication *)
+
+Definition mul x y :=
+  match x, y with
+    | 0, _ => 0
+    | _, 0 => 0
+    | Zpos x', Zpos y' => Zpos (x' * y')
+    | Zpos x', Zneg y' => Zneg (x' * y')
+    | Zneg x', Zpos y' => Zneg (x' * y')
+    | Zneg x', Zneg y' => Zpos (x' * y')
+  end.
+
+Infix "*" := mul : Z_scope.
+
+(** ** Subtraction of positive into Z *)
+
+Fixpoint pos_sub (x y:positive) {struct y} : Z :=
+  match x, y with
+    | p~1, q~1 => double (pos_sub p q)
+    | p~1, q~0 => succ_double (pos_sub p q)
+    | p~1, 1 => Zpos p~0
+    | p~0, q~1 => pred_double (pos_sub p q)
+    | p~0, q~0 => double (pos_sub p q)
+    | p~0, 1 => Zpos (Pos.pred_double p)
+    | 1, q~1 => Zneg q~0
+    | 1, q~0 => Zneg (Pos.pred_double q)
+    | 1, 1 => Z0
+  end%positive.
+
+(** ** Direct, easier to handle variants of successor and addition *)
+
+Definition succ' x :=
+  match x with
+    | 0 => 1
+    | Zpos x' => Zpos (Pos.succ x')
+    | Zneg x' => pos_sub 1 x'
+  end.
+
+Definition pred' x :=
+  match x with
+    | 0 => -1
+    | Zpos x' => pos_sub x' 1
+    | Zneg x' => Zneg (Pos.succ x')
+  end.
+
+Definition add' x y :=
+  match x, y with
+    | 0, y => y
+    | x, 0 => x
+    | Zpos x', Zpos y' => Zpos (x' + y')
+    | Zpos x', Zneg y' => pos_sub x' y'
+    | Zneg x', Zpos y' => pos_sub y' x'
+    | Zneg x', Zneg y' => Zneg (x' + y')
+  end.
+
+(** ** Power function *)
+
+Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1.
+
+Definition pow x y :=
+  match y with
+    | Zpos p => pow_pos x p
+    | 0 => 1
+    | Zneg _ => 0
+  end.
+
+Infix "^" := pow : Z_scope.
+
+(** ** Comparison *)
+
+Definition compare x y :=
+  match x, y with
+    | 0, 0 => Eq
+    | 0, Zpos y' => Lt
+    | 0, Zneg y' => Gt
+    | Zpos x', 0 => Gt
+    | Zpos x', Zpos y' => (x' ?= y')%positive
+    | Zpos x', Zneg y' => Gt
+    | Zneg x', 0 => Lt
+    | Zneg x', Zpos y' => Lt
+    | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive)
+  end.
+
+Infix "?=" := compare (at level 70, no associativity) : Z_scope.
+
+(** ** Sign function *)
+
+Definition sgn z :=
+  match z with
+    | 0 => 0
+    | Zpos p => 1
+    | Zneg p => -1
+  end.
+
+(** Boolean equality and comparisons *)
+
+Definition leb x y :=
+  match x ?= y with
+    | Gt => false
+    | _ => true
+  end.
+
+Definition geb x y := (* TODO : to provide ? to modify ? *)
+  match x ?= y with
+    | Lt => false
+    | _ => true
+  end.
+
+Definition ltb x y :=
+  match x ?= y with
+    | Lt => true
+    | _ => false
+  end.
+
+Definition gtb x y := (* TODO : to provide ? to modify ? *)
+  match x ?= y with
+    | Gt => true
+    | _ => false
+  end.
+
+(** Nota: this [eqb] is not convertible with the generated [Z_beq],
+    since the underlying [Pos.eqb] differs from [positive_beq]
+    (cf BinIntDef). *)
+
+Fixpoint eqb x y :=
+  match x, y with
+    | 0, 0 => true
+    | Zpos p, Zpos q => Pos.eqb p q
+    | Zneg p, Zneg q => Pos.eqb p q
+    | _, _ => false
+  end.
+
+Infix "=?" := eqb (at level 70, no associativity) : Z_scope.
+Infix "<=?" := leb (at level 70, no associativity) : Z_scope.
+Infix "<?" := ltb (at level 70, no associativity) : Z_scope.
+Infix ">=?" := geb (at level 70, no associativity) : Z_scope.
+Infix ">?" := gtb (at level 70, no associativity) : Z_scope.
+
+(** ** Minimum and maximum *)
+
+Definition max n m :=
+  match n ?= m with
+    | Eq | Gt => n
+    | Lt => m
+  end.
+
+Definition min n m :=
+  match n ?= m with
+    | Eq | Lt => n
+    | Gt => m
+  end.
+
+(** ** Absolute value *)
+
+Definition abs z :=
+  match z with
+    | 0 => 0
+    | Zpos p => Zpos p
+    | Zneg p => Zpos p
+  end.
+
+(** ** Conversions *)
+
+(** From [Z] to [nat] via absolute value *)
+
+Definition abs_nat (z:Z) : nat :=
+  match z with
+    | 0 => 0%nat
+    | Zpos p => Pos.to_nat p
+    | Zneg p => Pos.to_nat p
+  end.
+
+(** From [Z] to [N] via absolute value *)
+
+Definition abs_N (z:Z) : N :=
+  match z with
+    | Z0 => 0%N
+    | Zpos p => Npos p
+    | Zneg p => Npos p
+  end.
+
+(** From [Z] to [nat] by rounding negative numbers to 0 *)
+
+Definition to_nat (z:Z) : nat :=
+  match z with
+    | Zpos p => Pos.to_nat p
+    | _ => O
+  end.
+
+(** From [Z] to [N] by rounding negative numbers to 0 *)
+
+Definition to_N (z:Z) : N :=
+  match z with
+    | Zpos p => Npos p
+    | _ => 0%N
+  end.
+
+(** From [nat] to [Z] *)
+
+Definition of_nat (n:nat) : Z :=
+  match n with
+   | O => 0
+   | S n => Zpos (Pos.of_succ_nat n)
+  end.
+
+(** From [N] to [Z] *)
+
+Definition of_N (n:N) : Z :=
+  match n with
+    | N0 => 0
+    | Npos p => Zpos p
+  end.
+
+(** ** Iteration of a function
+
+    By convention, iterating a negative number of times is identity.
+*)
+
+Definition iter (n:Z) {A} (f:A -> A) (x:A) :=
+  match n with
+    | Zpos p => Pos.iter p f x
+    | _ => x
+  end.
+
+(** ** Euclidean divisions for binary integers *)
+
+(** Concerning the many possible variants of integer divisions,
+    see the headers of the generic files [ZDivFloor], [ZDivTrunc],
+    [ZDivEucl], and the article by R. Boute mentioned there.
+    We provide here two flavours, Floor and Trunc, while
+    the Euclid convention can be found in file Zeuclid.v
+    For non-zero b, they all satisfy [a = b*(a/b) + (a mod b)]
+    and [ |a mod b| < |b| ], but the sign of the modulo will differ
+    when [a<0] and/or [b<0].
+*)
+
+(** ** Floor division *)
+
+(** [div_eucl] provides a Truncated-Toward-Bottom (a.k.a Floor)
+  Euclidean division. Its projections are named [div] (noted "/")
+  and [modulo] (noted with an infix "mod").
+  These functions correspond to the `div` and `mod` of Haskell.
+  This is the historical convention of Coq.
+
+  The main properties of this convention are :
+    - we have [sgn (a mod b) = sgn (b)]
+    - [div a b] is the greatest integer smaller or equal to the exact
+      fraction [a/b].
+    - there is no easy sign rule.
+
+  In addition, note that we arbitrary take [a/0 = 0] and [a mod 0 = 0].
+*)
+
+(** First, a division for positive numbers. Even if the second
+   argument is a Z, the answer is arbitrary is it isn't a Zpos. *)
+
+Fixpoint pos_div_eucl (a:positive) (b:Z) : Z * Z :=
+  match a with
+    | xH => if b >=? 2 then (0, 1) else (1, 0)
+    | xO a' =>
+      let (q, r) := pos_div_eucl a' b in
+      let r' := 2 * r in
+      if b >? r' then (2 * q, r') else (2 * q + 1, r' - b)
+    | xI a' =>
+      let (q, r) := pos_div_eucl a' b in
+      let r' := 2 * r + 1 in
+      if b >? r' then (2 * q, r') else (2 * q + 1, r' - b)
+  end.
+
+(** Then the general euclidean division *)
+
+Definition div_eucl (a b:Z) : Z * Z :=
+  match a, b with
+    | 0, _ => (0, 0)
+    | _, 0 => (0, 0)
+    | Zpos a', Zpos _ => pos_div_eucl a' b
+    | Zneg a', Zpos _ =>
+      let (q, r) := pos_div_eucl a' b in
+	match r with
+	  | 0 => (- q, 0)
+	  | _ => (- (q + 1), b - r)
+	end
+    | Zneg a', Zneg b' =>
+      let (q, r) := pos_div_eucl a' (Zpos b') in (q, - r)
+    | Zpos a', Zneg b' =>
+      let (q, r) := pos_div_eucl a' (Zpos b') in
+	match r with
+	  | 0 => (- q, 0)
+	  | _ => (- (q + 1), b + r)
+	end
+  end.
+
+Definition div (a b:Z) : Z := let (q, _) := div_eucl a b in q.
+Definition modulo (a b:Z) : Z := let (_, r) := div_eucl a b in r.
+
+Infix "/" := div : Z_scope.
+Infix "mod" := modulo (at level 40, no associativity) : Z_scope.
+
+
+(** ** Trunc Division *)
+
+(** [quotrem] provides a Truncated-Toward-Zero Euclidean division.
+  Its projections are named [quot] (noted "÷") and [rem].
+  These functions correspond to the `quot` and `rem` of Haskell.
+  This division convention is used in most programming languages,
+  e.g. Ocaml.
+
+  With this convention:
+   - we have [sgn(a rem b) = sgn(a)]
+   - sign rule for division: [quot (-a) b = quot a (-b) = -(quot a b)]
+   - and for modulo: [a rem (-b) = a rem b] and [(-a) rem b = -(a rem b)]
+
+ Note that we arbitrary take here [quot a 0 = 0] and [a rem 0 = a].
+*)
+
+Definition quotrem (a b:Z) : Z * Z :=
+  match a, b with
+   | 0,  _ => (0, 0)
+   | _, 0  => (0, a)
+   | Zpos a, Zpos b =>
+     let (q, r) := N.pos_div_eucl a (Npos b) in (of_N q, of_N r)
+   | Zneg a, Zpos b =>
+     let (q, r) := N.pos_div_eucl a (Npos b) in (-of_N q, - of_N r)
+   | Zpos a, Zneg b =>
+     let (q, r) := N.pos_div_eucl a (Npos b) in (-of_N q, of_N r)
+   | Zneg a, Zneg b =>
+     let (q, r) := N.pos_div_eucl a (Npos b) in (of_N q, - of_N r)
+  end.
+
+Definition quot a b := fst (quotrem a b).
+Definition rem a b := snd (quotrem a b).
+
+Infix "÷" := quot (at level 40, left associativity) : Z_scope.
+(** No infix notation for rem, otherwise it becomes a keyword *)
+
+
+(** ** Parity functions *)
+
+Definition even z :=
+  match z with
+    | 0 => true
+    | Zpos (xO _) => true
+    | Zneg (xO _) => true
+    | _ => false
+  end.
+
+Definition odd z :=
+  match z with
+    | 0 => false
+    | Zpos (xO _) => false
+    | Zneg (xO _) => false
+    | _ => true
+  end.
+
+
+(** ** Division by two *)
+
+(** [div2] performs rounding toward bottom, it is hence a particular
+   case of [div], and for all relative number [n] we have:
+   [n = 2 * div2 n + if odd n then 1 else 0].  *)
+
+Definition div2 z :=
+ match z with
+   | 0 => 0
+   | Zpos 1 => 0
+   | Zpos p => Zpos (Pos.div2 p)
+   | Zneg p => Zneg (Pos.div2_up p)
+ end.
+
+(** [quot2] performs rounding toward zero, it is hence a particular
+   case of [quot], and for all relative number [n] we have:
+   [n = 2 * quot2 n + if odd n then sgn n else 0].  *)
+
+Definition quot2 (z:Z) :=
+  match z with
+    | 0 => 0
+    | Zpos 1 => 0
+    | Zpos p => Zpos (Pos.div2 p)
+    | Zneg 1 => 0
+    | Zneg p => Zneg (Pos.div2 p)
+  end.
+
+(** NB: [Z.quot2] used to be named [Zdiv2] in Coq <= 8.3 *)
+
+
+(** * Base-2 logarithm *)
+
+Definition log2 z :=
+  match z with
+    | Zpos (p~1) => Zpos (Pos.size p)
+    | Zpos (p~0) => Zpos (Pos.size p)
+    | _ => 0
+  end.
+
+
+(** ** Square root *)
+
+Definition sqrtrem n :=
+ match n with
+  | 0 => (0, 0)
+  | Zpos p =>
+    match Pos.sqrtrem p with
+     | (s, IsPos r) => (Zpos s, Zpos r)
+     | (s, _) => (Zpos s, 0)
+    end
+  | Zneg _ => (0,0)
+ end.
+
+Definition sqrt n :=
+ match n with
+  | Zpos p => Zpos (Pos.sqrt p)
+  | _ => 0
+ end.
+
+
+(** ** Greatest Common Divisor *)
+
+Definition gcd a b :=
+  match a,b with
+    | 0, _ => abs b
+    | _, 0 => abs a
+    | Zpos a, Zpos b => Zpos (Pos.gcd a b)
+    | Zpos a, Zneg b => Zpos (Pos.gcd a b)
+    | Zneg a, Zpos b => Zpos (Pos.gcd a b)
+    | Zneg a, Zneg b => Zpos (Pos.gcd a b)
+  end.
+
+(** A generalized gcd, also computing division of a and b by gcd. *)
+
+Definition ggcd a b : Z*(Z*Z) :=
+  match a,b with
+    | 0, _ => (abs b,(0, sgn b))
+    | _, 0 => (abs a,(sgn a, 0))
+    | Zpos a, Zpos b =>
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zpos bb))
+    | Zpos a, Zneg b =>
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zneg bb))
+    | Zneg a, Zpos b =>
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zpos bb))
+    | Zneg a, Zneg b =>
+       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zneg bb))
+  end.
+
+
+(** ** Bitwise functions *)
+
+(** When accessing the bits of negative numbers, all functions
+  below will use the two's complement representation. For instance,
+  [-1] will correspond to an infinite stream of true bits. If this
+  isn't what you're looking for, you can use [abs] first and then
+  access the bits of the absolute value.
+*)
+
+(** [testbit] : accessing the [n]-th bit of a number [a].
+    For negative [n], we arbitrarily answer [false]. *)
+
+Definition testbit a n :=
+ match n with
+   | 0 => odd a
+   | Zpos p =>
+     match a with
+       | 0 => false
+       | Zpos a => Pos.testbit a (Npos p)
+       | Zneg a => negb (N.testbit (Pos.pred_N a) (Npos p))
+     end
+   | Zneg _ => false
+ end.
+
+(** Shifts
+
+   Nota: a shift to the right by [-n] will be a shift to the left
+   by [n], and vice-versa.
+
+   For fulfilling the two's complement convention, shifting to
+   the right a negative number should correspond to a division
+   by 2 with rounding toward bottom, hence the use of [div2]
+   instead of [quot2].
+*)
+
+Definition shiftl a n :=
+ match n with
+   | 0 => a
+   | Zpos p => Pos.iter p (mul 2) a
+   | Zneg p => Pos.iter p div2 a
+ end.
+
+Definition shiftr a n := shiftl a (-n).
+
+(** Bitwise operations [lor] [land] [ldiff] [lxor] *)
+
+Definition lor a b :=
+ match a, b with
+   | 0, _ => b
+   | _, 0 => a
+   | Zpos a, Zpos b => Zpos (Pos.lor a b)
+   | Zneg a, Zpos b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N a) (Npos b)))
+   | Zpos a, Zneg b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N b) (Npos a)))
+   | Zneg a, Zneg b => Zneg (N.succ_pos (N.land (Pos.pred_N a) (Pos.pred_N b)))
+ end.
+
+Definition land a b :=
+ match a, b with
+   | 0, _ => 0
+   | _, 0 => 0
+   | Zpos a, Zpos b => of_N (Pos.land a b)
+   | Zneg a, Zpos b => of_N (N.ldiff (Npos b) (Pos.pred_N a))
+   | Zpos a, Zneg b => of_N (N.ldiff (Npos a) (Pos.pred_N b))
+   | Zneg a, Zneg b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Pos.pred_N b)))
+ end.
+
+Definition ldiff a b :=
+ match a, b with
+   | 0, _ => 0
+   | _, 0 => a
+   | Zpos a, Zpos b => of_N (Pos.ldiff a b)
+   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Npos b)))
+   | Zpos a, Zneg b => of_N (N.land (Npos a) (Pos.pred_N b))
+   | Zneg a, Zneg b => of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a))
+ end.
+
+Definition lxor a b :=
+ match a, b with
+   | 0, _ => b
+   | _, 0 => a
+   | Zpos a, Zpos b => of_N (Pos.lxor a b)
+   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lxor (Pos.pred_N a) (Npos b)))
+   | Zpos a, Zneg b => Zneg (N.succ_pos (N.lxor (Npos a) (Pos.pred_N b)))
+   | Zneg a, Zneg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
+ end.
+
+End Z.
\ No newline at end of file
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index a4c8d4796..76308e60b 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -36,17 +36,12 @@ Proof.
   intro; apply Zcompare_rect.
 Defined.
 
+Notation Z_eq_dec := Z.eq_dec (only parsing).
+
 Section decidability.
 
   Variables x y : Z.
 
-  (** * Decidability of equality on binary integers *)
-
-  Definition Z_eq_dec : {x = y} + {x <> y}.
-  Proof.
-    decide equality; apply positive_eq_dec.
-  Defined.
-
   (** * Decidability of order on binary integers *)
 
   Definition Z_lt_dec : {x < y} + {~ x < y}.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index a90b5bd69..77cae88fe 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -21,8 +21,8 @@ Open Local Scope Z_scope.
 (**********************************************************************)
 (** * Properties of absolute value *)
 
-Notation Zabs_eq := Zabs_eq (only parsing). (* 0 <= n -> Zabs n = n *)
-Notation Zabs_non_eq := Zabs_non_eq (only parsing). (* n <= 0 -> Zabs n = -n *)
+Notation Zabs_eq := Z.abs_eq (only parsing). (* 0 <= n -> Zabs n = n *)
+Notation Zabs_non_eq := Z.abs_neq (only parsing). (* n <= 0 -> Zabs n = -n *)
 
 Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n.
 Proof.
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 45fcc17be..d91843aef 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -33,29 +33,10 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x).
 (**********************************************************************)
 (** * Boolean comparisons of binary integers *)
 
-Definition Zle_bool (x y:Z) :=
-  match x ?= y with
-    | Gt => false
-    | _ => true
-  end.
-
-Definition Zge_bool (x y:Z) :=
-  match x ?= y with
-    | Lt => false
-    | _ => true
-  end.
-
-Definition Zlt_bool (x y:Z) :=
-  match x ?= y with
-    | Lt => true
-    | _ => false
-  end.
-
-Definition Zgt_bool (x y:Z) :=
-  match x ?= y with
-    | Gt => true
-    | _ => false
-  end.
+Notation Zle_bool := Z.leb (only parsing).
+Notation Zge_bool := Z.geb (only parsing).
+Notation Zlt_bool := Z.ltb (only parsing).
+Notation Zgt_bool := Z.gtb (only parsing).
 
 Definition Zeq_bool (x y:Z) :=
   match x ?= y with
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index becd34f11..d07f52891 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -77,9 +77,7 @@ Qed.
 Lemma Zcompare_Lt_trans :
   forall n m p:Z, (n ?= m) = Lt -> (m ?= p) = Lt -> (n ?= p) = Lt.
 Proof.
- intros n m p; destruct n,m,p; simpl; try discriminate; trivial.
- eapply Plt_trans; eauto.
- rewrite <- 3 Pos.compare_antisym; simpl. intros; eapply Plt_trans; eauto.
+ exact Z.lt_trans.
 Qed.
 
 Lemma Zcompare_Gt_trans :
@@ -94,78 +92,38 @@ Qed.
 
 (** * Comparison and opposite *)
 
-Lemma Zcompare_opp : forall n m:Z, (n ?= m) = (- m ?= - n).
+Lemma Zcompare_opp : forall n m, (n ?= m) = (- m ?= - n).
 Proof.
- destruct n, m; simpl; trivial; intros; now rewrite <- Pos.compare_antisym.
+ symmetry. apply Z.compare_opp.
 Qed.
 
 (** * Comparison first-order specification *)
 
 Lemma Zcompare_Gt_spec :
-  forall n m:Z, (n ?= m) = Gt ->  exists h, n + - m = Zpos h.
+  forall n m, (n ?= m) = Gt ->  exists h, n + - m = Zpos h.
 Proof.
- intros [|p|p] [|q|q]; simpl; try discriminate.
- now exists q.
- now exists p.
- intros GT. exists (p-q)%positive. now rewrite GT.
- now exists (p+q)%positive.
- intros LT. apply CompOpp_iff in LT. simpl in LT.
- exists (q-p)%positive. now rewrite LT.
+ intros n m H. rewrite Z.compare_sub in H. unfold Z.sub in H.
+ destruct (n+-m) as [|p|p]; try discriminate. now exists p.
 Qed.
 
 (** * Comparison and addition *)
 
-Local Hint Resolve Pcompare_refl.
-
-Lemma weak_Zcompare_plus_compat :
-  forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m).
+Lemma Zcompare_plus_compat : forall n m p, (p + n ?= p + m) = (n ?= m).
 Proof.
- intros [|x|x] [|y|y] z; simpl; trivial; try apply ZC2;
-  try apply Plt_plus_r.
- case Pcompare_spec; intros E0; trivial; try apply ZC2;
-  now apply Pminus_decr.
- apply Pplus_compare_mono_l.
- case Pcompare_spec; intros E0; trivial; try apply ZC2.
-  apply Plt_trans with z. now apply Pminus_decr. apply Plt_plus_r.
- case Pcompare_spec; intros E0; trivial; try apply ZC2.
-  now apply Pminus_decr.
- case Pcompare_spec; intros E0; trivial; try apply ZC2.
-  apply Plt_trans with z. now apply Pminus_decr. apply Plt_plus_r.
- case Pcompare_spec; intros E0; simpl; subst.
-  now case Pcompare_spec.
-  case Pcompare_spec; intros E1; simpl; subst; trivial.
-  now rewrite <- Pos.compare_antisym.
-  f_equal.
-  apply Pminus_compare_mono_r; trivial.
-  rewrite <- Pos.compare_antisym. symmetry. now apply Plt_trans with z.
-  case Pcompare_spec; intros E1; simpl; subst; trivial.
-  now rewrite E0.
-  symmetry. apply CompOpp_iff. now apply Plt_trans with z.
-  rewrite <- Pos.compare_antisym.
-  apply Pminus_compare_mono_l; trivial.
-Qed.
-
-Lemma Zcompare_plus_compat : forall n m p:Z, (p + n ?= p + m) = (n ?= m).
-Proof.
- intros x y [|z|z]; trivial.
- apply weak_Zcompare_plus_compat.
- rewrite (Zcompare_opp x y), Zcompare_opp, 2 Zopp_plus_distr, Zopp_neg.
- apply weak_Zcompare_plus_compat.
+ intros. apply Z.add_compare_mono_l.
 Qed.
 
 Lemma Zplus_compare_compat :
   forall (r:comparison) (n m p q:Z),
     (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.
 Proof.
- intros [ | | ] x y z t H H'.
- apply Zcompare_Eq_eq in H. apply Zcompare_Eq_eq in H'. subst.
-  apply Zcompare_refl.
- apply Zcompare_Lt_trans with (y+z).
- now rewrite 2 (Zplus_comm _ z), Zcompare_plus_compat.
- now rewrite Zcompare_plus_compat.
- apply Zcompare_Gt_trans with (y+z).
- now rewrite 2 (Zplus_comm _ z), Zcompare_plus_compat.
- now rewrite Zcompare_plus_compat.
+ intros r n m p q.
+ rewrite (Z.compare_sub n), (Z.compare_sub p), (Z.compare_sub (n+p)).
+ unfold Z.sub. rewrite Z.BootStrap.opp_add_distr.
+ rewrite <- Z.BootStrap.add_assoc, (Z.BootStrap.add_assoc p).
+ rewrite (Z.BootStrap.add_comm p (-m)).
+ rewrite <- Z.BootStrap.add_assoc,  (Z.BootStrap.add_assoc n).
+ destruct (n+-m), (p+-q); simpl; intros; now subst.
 Qed.
 
 Lemma Zcompare_succ_Gt : forall n:Z, (Zsucc n ?= n) = Gt.
@@ -176,17 +134,10 @@ Qed.
 
 Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m+1) <> Lt.
 Proof.
- intros x y; split; intros H.
- (* -> *)
- destruct (Zcompare_Gt_spec _ _ H) as (h,EQ).
- replace x with (y+Zpos h) by (rewrite <- EQ; apply Zplus_minus).
- rewrite Zcompare_plus_compat. apply Plt_1.
- (* <- *)
- assert (H' := Zcompare_succ_Gt y).
- destruct (Zcompare_spec x (y+1)) as [->|LT|GT]; trivial.
-  now elim H.
-  apply Zcompare_Gt_Lt_antisym in GT.
-   apply Zcompare_Gt_trans with (y+1); trivial.
+ intros n m. rewrite 2 (Z.compare_sub n).
+ unfold Z.sub. rewrite Z.BootStrap.opp_add_distr.
+ rewrite Z.BootStrap.add_assoc.
+ destruct (n+-m) as [|[ | | ]|]; simpl; easy'.
 Qed.
 
 (** * Successor and comparison *)
@@ -316,62 +267,13 @@ Proof.
     apply Zmult_compare_compat_l; assumption.
 Qed.
 
-(*************************)
-(** * Basic properties of minimum and maximum *)
-
-Lemma Zmax_l : forall x y, y<=x -> Zmax x y = x.
-Proof.
- unfold Zle, Zmax. intros x y. rewrite <- (Zcompare_antisym x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmax_r : forall x y, x<=y -> Zmax x y = y.
-Proof.
- unfold Zle, Zmax. intros x y. generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmin_l : forall x y, x<=y -> Zmin x y = x.
-Proof.
- unfold Zle, Zmin. intros x y. generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
-Lemma Zmin_r : forall x y, y<=x -> Zmin x y = y.
-Proof.
- unfold Zle, Zmin. intros x y.
- rewrite <- (Zcompare_antisym x y). generalize (Zcompare_Eq_eq x y).
- destruct (x ?= y); intuition.
-Qed.
-
+Notation Zmin_l := Z.min_l (only parsing).
+Notation Zmin_r := Z.min_r (only parsing).
+Notation Zmax_l := Z.max_l (only parsing).
+Notation Zmax_r := Z.max_r (only parsing).
+Notation Zabs_eq := Z.abs_eq (only parsing).
+Notation Zabs_non_eq := Z.abs_neq (only parsing).
+Notation Zsgn_0 := Z.sgn_null (only parsing).
+Notation Zsgn_1 := Z.sgn_pos (only parsing).
+Notation Zsgn_m1 := Z.sgn_neg (only parsing).
 
-(**************************)
-(** * Basic properties of [Zabs] *)
-
-Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n.
-Proof.
- destruct n; auto. now destruct 1.
-Qed.
-
-Lemma Zabs_non_eq : forall n:Z, n <= 0 -> Zabs n = - n.
-Proof.
- destruct n; auto. now destruct 1.
-Qed.
-
-(**************************)
-(** * Basic properties of [Zsign] *)
-
-Lemma Zsgn_0 : forall x, x = 0 -> Zsgn x = 0.
-Proof.
- intros. now subst.
-Qed.
-
-Lemma Zsgn_1 : forall x, 0 < x -> Zsgn x = 1.
-Proof.
- destruct x; auto; discriminate.
-Qed.
-
-Lemma Zsgn_m1 : forall x, x < 0 -> Zsgn x = -1.
-Proof.
- destruct x; auto; discriminate.
-Qed.
diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v
index a04719e52..1fff96dd1 100644
--- a/theories/ZArith/Zdigits_def.v
+++ b/theories/ZArith/Zdigits_def.v
@@ -13,88 +13,13 @@ Require Import Bool BinPos BinNat BinInt Znat Zeven Zpow_def
 
 Local Open Scope Z_scope.
 
-(** When accessing the bits of negative numbers, all functions
-  below will use the two's complement representation. For instance,
-  [-1] will correspond to an infinite stream of true bits. If this
-  isn't what you're looking for, you can use [Zabs] first and then
-  access the bits of the absolute value.
-*)
-
-(** [Ztestbit] : accessing the [n]-th bit of a number [a].
-    For negative [n], we arbitrarily answer [false]. *)
-
-Definition Ztestbit a n :=
- match n with
-   | 0 => Zodd_bool a
-   | Zpos p => match a with
-                 | 0 => false
-                 | Zpos a => Pos.testbit a (Npos p)
-                 | Zneg a => negb (N.testbit (Pos.pred_N a) (Npos p))
-               end
-   | Zneg _ => false
- end.
-
-(** Shifts
-
-   Nota: a shift to the right by [-n] will be a shift to the left
-   by [n], and vice-versa.
-
-   For fulfilling the two's complement convention, shifting to
-   the right a negative number should correspond to a division
-   by 2 with rounding toward bottom, hence the use of [Zdiv2]
-   instead of [Zquot2].
-*)
-
-Definition Zshiftl a n :=
- match n with
-   | 0 => a
-   | Zpos p => iter_pos p _ (Zmult 2) a
-   | Zneg p => iter_pos p _ Zdiv2 a
- end.
-
-Definition Zshiftr a n := Zshiftl a (-n).
-
-(** Bitwise operations Zor Zand Zdiff Zxor *)
-
-Definition Zor a b :=
- match a, b with
-   | 0, _ => b
-   | _, 0 => a
-   | Zpos a, Zpos b => Zpos (Pos.lor a b)
-   | Zneg a, Zpos b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N a) (Npos b)))
-   | Zpos a, Zneg b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N b) (Npos a)))
-   | Zneg a, Zneg b => Zneg (N.succ_pos (N.land (Pos.pred_N a) (Pos.pred_N b)))
- end.
-
-Definition Zand a b :=
- match a, b with
-   | 0, _ => 0
-   | _, 0 => 0
-   | Zpos a, Zpos b => Z_of_N (Pos.land a b)
-   | Zneg a, Zpos b => Z_of_N (N.ldiff (Npos b) (Pos.pred_N a))
-   | Zpos a, Zneg b => Z_of_N (N.ldiff (Npos a) (Pos.pred_N b))
-   | Zneg a, Zneg b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Pos.pred_N b)))
- end.
-
-Definition Zdiff a b :=
- match a, b with
-   | 0, _ => 0
-   | _, 0 => a
-   | Zpos a, Zpos b => Z_of_N (Pos.ldiff a b)
-   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Npos b)))
-   | Zpos a, Zneg b => Z_of_N (N.land (Npos a) (Pos.pred_N b))
-   | Zneg a, Zneg b => Z_of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a))
- end.
-
-Definition Zxor a b :=
- match a, b with
-   | 0, _ => b
-   | _, 0 => a
-   | Zpos a, Zpos b => Z_of_N (Pos.lxor a b)
-   | Zneg a, Zpos b => Zneg (N.succ_pos (N.lxor (Pos.pred_N a) (Npos b)))
-   | Zpos a, Zneg b => Zneg (N.succ_pos (N.lxor (Npos a) (Pos.pred_N b)))
-   | Zneg a, Zneg b => Z_of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
- end.
+Notation Ztestbit := Z.testbit (only parsing).
+Notation Zshiftr := Z.shiftr (only parsing).
+Notation Zshiftl := Z.shiftl (only parsing).
+Notation Zor := Z.lor (only parsing).
+Notation Zand := Z.land (only parsing).
+Notation Zdiff := Z.ldiff (only parsing).
+Notation Zxor := Z.lxor (only parsing).
 
 
 (** Conversions between [Ztestbit] and [Ntestbit] *)
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index be29c8cb5..a5f42d6d1 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -11,9 +11,9 @@
 
 (** Initial Contribution by Claude Marché and Xavier Urbain *)
 
-Require Export ZArith_base Zdiv_def.
+Require Export ZArith_base.
 Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
-Require ZDivFloor.
+Require Import Zdiv_def.
 Local Open Scope Z_scope.
 
 (** The definition and initial properties are now in file [Zdiv_def] *)
diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v
index e38bec175..0f375e144 100644
--- a/theories/ZArith/Zdiv_def.v
+++ b/theories/ZArith/Zdiv_def.v
@@ -9,292 +9,29 @@
 Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Znat.
 Local Open Scope Z_scope.
 
-(** * Definitions of divisions for binary integers *)
-
-(** Concerning the many possible variants of integer divisions, see:
-
-    R. Boute, "The Euclidean definition of the functions div and mod",
-    ACM Transactions on Programming Languages and Systems,
-    Vol. 14, No.2, pp. 127-144, April 1992.
-
-   We provide here two flavours:
-
-    - convention Floor (F) : [Zdiv_eucl], [Zdiv], [Zmod]
-    - convention Trunc (T) : [Zquotrem], [Zquot], [Zrem]
-
-   A third one, the Euclid (E) convention, can be found in file
-   Zeuclid.v
-
-   For non-zero b, they all satisfy [a = b*(a/b) + (a mod b)]
-   and [ |a mod b| < |b| ], but the sign of the modulo will differ
-   when [a<0] and/or [b<0].
-
-*)
-
-(** * Floor *)
-
-(** [Zdiv_eucl] provides a Truncated-Toward-Bottom (a.k.a Floor)
-  Euclidean division. Its projections are named [Zdiv] and [Zmod].
-  These functions correspond to the `div` and `mod` of Haskell.
-  This is the historical convention of Coq.
-
-  The main properties of this convention are :
-    - we have [sgn (a mod b) = sgn (b)]
-    - [div a b] is the greatest integer smaller or equal to the exact
-      fraction [a/b].
-    - there is no easy sign rule.
-
-  In addition, note that we arbitrary take [a/0 = 0] and [a mod 0 = 0].
-*)
-
-(** First, a division for positive numbers. Even if the second
-   argument is a Z, the answer is arbitrary is it isn't a Zpos. *)
-
-Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z :=
-  match a with
-    | xH => if Zge_bool b 2 then (0, 1) else (1, 0)
-    | xO a' =>
-      let (q, r) := Zdiv_eucl_POS a' b in
-	let r' := 2 * r in
-	  if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b)
-    | xI a' =>
-      let (q, r) := Zdiv_eucl_POS a' b in
-	let r' := 2 * r + 1 in
-	  if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b)
-  end.
-
-(** Then the general euclidean division *)
-
-Definition Zdiv_eucl (a b:Z) : Z * Z :=
-  match a, b with
-    | 0, _ => (0, 0)
-    | _, 0 => (0, 0)
-    | Zpos a', Zpos _ => Zdiv_eucl_POS a' b
-    | Zneg a', Zpos _ =>
-      let (q, r) := Zdiv_eucl_POS a' b in
-	match r with
-	  | 0 => (- q, 0)
-	  | _ => (- (q + 1), b - r)
-	end
-    | Zneg a', Zneg b' =>
-      let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r)
-    | Zpos a', Zneg b' =>
-      let (q, r) := Zdiv_eucl_POS a' (Zpos b') in
-	match r with
-	  | 0 => (- q, 0)
-	  | _ => (- (q + 1), b + r)
-	end
-  end.
-
-Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q.
-Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r.
-
-Infix "/" := Zdiv : Z_scope.
-Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
-
-
-(** * Trunc *)
-
-(** [Zquotrem] provides a Truncated-Toward-Zero Euclidean division.
-  Its projections are named [Zquot] and [Zrem]. These functions
-  correspond to the `quot` and `rem` of Haskell, and this division
-  convention is used in most programming languages, e.g. Ocaml.
-
-  With this convention:
-   - we have [sgn(a rem b) = sgn(a)]
-   - sign rule for division: [quot (-a) b = quot a (-b) = -(quot a b)]
-   - and for modulo: [a rem (-b) = a rem b] and [(-a) rem b = -(a rem b)]
-
- Note that we arbitrary take here [quot a 0 = 0] and [a rem 0 = a].
-*)
-
-Definition Zquotrem (a b:Z) : Z * Z :=
-  match a, b with
-   | 0,  _ => (0, 0)
-   | _, 0  => (0, a)
-   | Zpos a, Zpos b =>
-     let (q, r) := N.pos_div_eucl a (Npos b) in (Z_of_N q, Z_of_N r)
-   | Zneg a, Zpos b =>
-     let (q, r) := N.pos_div_eucl a (Npos b) in (-Z_of_N q, - Z_of_N r)
-   | Zpos a, Zneg b =>
-     let (q, r) := N.pos_div_eucl a (Npos b) in (-Z_of_N q, Z_of_N r)
-   | Zneg a, Zneg b =>
-     let (q, r) := N.pos_div_eucl a (Npos b) in (Z_of_N q, - Z_of_N r)
-  end.
-
-Definition Zquot a b := fst (Zquotrem a b).
-Definition Zrem a b := snd (Zquotrem a b).
-
-Infix "÷" := Zquot (at level 40, left associativity) : Z_scope.
-(** No infix notation for rem, otherwise it becomes a keyword *)
-
-(** * Correctness proofs *)
-
-(** Correctness proofs for Trunc *)
+Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
+Notation Zdiv_eucl := Z.div_eucl (only parsing).
+Notation Zdiv := Z.div (only parsing).
+Notation Zmod := Z.modulo (only parsing).
+Notation Zquotrem := Z.quotrem (only parsing).
+Notation Zquot := Z.quot (only parsing).
+Notation Zrem := Z.rem (only parsing).
 
 Lemma Zdiv_eucl_POS_eq : forall a b, 0 < b ->
   let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r.
 Proof.
- intros a b Hb.
- induction a; cbv beta iota delta [Zdiv_eucl_POS]; fold Zdiv_eucl_POS.
- (* ~1 *)
- destruct Zdiv_eucl_POS as (q,r); cbv zeta.
- rewrite Zpos_xI, IHa, Zmult_plus_distr_r, Zmult_permute.
- destruct Zgt_bool.
- now rewrite Zplus_assoc.
- now rewrite Zmult_plus_distr_r, Zmult_1_r, <- !Zplus_assoc, Zplus_minus.
- (* ~0 *)
- destruct Zdiv_eucl_POS as (q,r); cbv zeta.
- rewrite (Zpos_xO a), IHa, Zmult_plus_distr_r, Zmult_permute.
- destruct Zgt_bool; trivial.
- now rewrite Zmult_plus_distr_r, Zmult_1_r, <- !Zplus_assoc, Zplus_minus.
- (* ~1 *)
- generalize (Zge_cases b 2); destruct Zge_bool; intros Hb'.
- now rewrite Zmult_0_r.
- replace b with 1. reflexivity.
- apply Zle_antisym. now apply Zlt_le_succ in Hb. now apply Zlt_succ_le.
-Qed.
-
-Lemma Zdiv_eucl_eq : forall a b, b<>0 ->
- let (q, r) := Zdiv_eucl a b in a = b * q + r.
-Proof.
- intros [ |a|a] [ |b|b]; unfold Zdiv_eucl; trivial;
-  (now destruct 1) || intros _;
-  generalize (Zdiv_eucl_POS_eq a (Zpos b) (eq_refl _));
-  destruct Zdiv_eucl_POS as (q,r); try change (Zneg a) with (-Zpos a);
-  intros ->.
- (* Zpos Zpos *)
- reflexivity.
- (* Zpos Zneg *)
- rewrite <- (Zopp_neg b), Zmult_opp_comm.
- destruct r as [ |r|r]; trivial.
- rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
- now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
- rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
- now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
- (* Zneg Zpos *)
- rewrite (Zopp_plus_distr _ r), Zopp_mult_distr_r.
- destruct r as [ |r|r]; trivial; unfold Zminus.
- rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
- now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
- rewrite Zopp_plus_distr, Zmult_plus_distr_r, <- Zplus_assoc. f_equal.
- now rewrite <- Zmult_opp_comm, Zmult_1_r, Zplus_assoc, Zplus_opp_l.
- (* Zneg Zneg *)
- now rewrite (Zopp_plus_distr _ r), Zopp_mult_distr_l.
-Qed.
-
-Lemma Z_div_mod_eq_full : forall a b, b<>0 -> a = b*(a/b) + (a mod b).
-Proof.
- intros a b Hb. generalize (Zdiv_eucl_eq a b Hb).
- unfold Zdiv, Zmod. now destruct Zdiv_eucl.
-Qed.
-
-Lemma Zmod_POS_bound : forall a b, 0<b -> 0 <= snd (Zdiv_eucl_POS a b) < b.
-Proof.
- assert (AUX : forall a p, a < Zpos (p~0) -> a - Zpos p < Zpos p).
-  intros. unfold Zminus. apply Zlt_plus_swap. unfold Zminus.
-  now rewrite Zopp_involutive, Zplus_diag_eq_mult_2, Zmult_comm.
- intros a [|b|b] Hb; discriminate Hb || clear Hb.
- induction a; cbv beta iota delta [Zdiv_eucl_POS]; fold Zdiv_eucl_POS.
- (* ~1 *)
- destruct Zdiv_eucl_POS as (q,r). cbv zeta.
- simpl in IHa; destruct IHa as (Hr,Hr').
- generalize (Zgt_cases (Zpos b) (2*r+1)). destruct Zgt_bool.
- unfold snd in *.
- split. apply Zplus_le_0_compat. now apply Zmult_le_0_compat. easy.
-  now apply Zgt_lt.
- unfold snd in *.
- split. now apply Zle_minus_le_0.
-  apply AUX.
-  destruct r as [|r|r]; try (now destruct Hr); try easy.
-  red. simpl. apply Pcompare_Gt_Lt. exact Hr'.
- (* ~0 *)
- destruct Zdiv_eucl_POS as (q,r). cbv zeta.
- simpl in IHa; destruct IHa as (Hr,Hr').
- generalize (Zgt_cases (Zpos b) (2*r)). destruct Zgt_bool.
- unfold snd in *.
- split. now apply Zmult_le_0_compat.
-  now apply Zgt_lt.
- unfold snd in *.
- split. now apply Zle_minus_le_0.
-  apply AUX.
-  destruct r as [|r|r]; try (now destruct Hr); try easy.
- (* 1 *)
- generalize (Zge_cases (Zpos b) 2). destruct Zge_bool; simpl.
- split. easy. now apply Zle_succ_l, Zge_le.
- now split.
-Qed.
-
-Lemma Zmod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b.
-Proof.
- intros a [|b|b] Hb; discriminate Hb || clear Hb.
- destruct a as [|a|a]; unfold Zmod, Zdiv_eucl.
- now split.
- now apply Zmod_POS_bound.
- generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)).
- destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr').
- destruct r as [|r|r]; (now destruct Hr) || clear Hr.
- now split.
- split. now apply Zlt_le_weak, Zlt_plus_swap.
- now apply Zlt_minus_simpl_swap.
-Qed.
-
-Lemma Zmod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0.
-Proof.
- intros a [|b|b] Hb; discriminate Hb || clear Hb.
- destruct a as [|a|a]; unfold Zmod, Zdiv_eucl.
- now split.
- generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)).
- destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr').
- destruct r as [|r|r]; (now destruct Hr) || clear Hr.
- now split.
- split. rewrite Zplus_comm. now apply (Zplus_lt_compat_r 0).
- rewrite Zplus_comm. apply Zle_plus_swap. simpl. now apply Zlt_le_weak.
- generalize (Zmod_POS_bound a (Zpos b) (eq_refl _)).
- destruct Zdiv_eucl_POS as (q,r). unfold snd. intros (Hr,Hr').
- split. red in Hr'. now rewrite Zcompare_opp in Hr'. now destruct r.
+ intros a b Hb. generalize (Z.pos_div_eucl_eq a b Hb).
+ destruct Z.pos_div_eucl. now rewrite Z.mul_comm.
 Qed.
 
-(** Correctness proofs for Floor *)
+Notation Zdiv_eucl_eq := Z.div_eucl_eq (only parsing).
+Notation Z_div_mod_eq_full := Z.div_mod (only parsing).
+Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).
+Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing).
+Notation Zmod_neg_bound := Z.mod_neg_bound (only parsing).
 
-Theorem Zquotrem_eq: forall a b,
-  let (q,r) := Zquotrem a b in a = q * b + r.
-Proof.
- destruct a, b; simpl; trivial;
- generalize (N.pos_div_eucl_spec p (Npos p0)); case N.pos_div_eucl; trivial;
-  intros q r H; try change (Zneg p) with (-Zpos p);
-  rewrite <- (Z_of_N_pos p), H, Z_of_N_plus, Z_of_N_mult; f_equal.
- now rewrite Zmult_opp_comm.
- now rewrite Zopp_plus_distr, Zopp_mult_distr_l.
- now rewrite Zopp_plus_distr, Zopp_mult_distr_r.
-Qed.
-
-Lemma Z_quot_rem_eq : forall a b, a = b*(a÷b) + Zrem a b.
-Proof.
- intros a b. rewrite Zmult_comm. generalize (Zquotrem_eq a b).
- unfold Zquot, Zrem. now destruct Zquotrem.
-Qed.
-
-Lemma Zrem_bound : forall a b, 0<=a -> 0<b -> 0 <= Zrem a b < b.
-Proof.
- intros a [|b|b] Ha Hb; discriminate Hb || clear Hb.
- destruct a as [|a|a]; (now destruct Ha) || clear Ha.
- compute. now split.
- unfold Zrem, Zquotrem.
- assert (H := N.pos_div_eucl_remainder a (Npos b)).
- destruct N.pos_div_eucl as (q,r); simpl.
- split. apply Z_of_N_le_0.
- destruct r; [ reflexivity | now apply H ].
-Qed.
-
-Lemma Zrem_opp_l : forall a b, Zrem (-a) b = - (Zrem a b).
-Proof.
- intros [|a|a] [|b|b]; trivial; unfold Zrem;
-  simpl; destruct N.pos_div_eucl; simpl; try rewrite Zopp_involutive; trivial.
-Qed.
-
-Lemma Zrem_opp_r : forall a b, Zrem a (-b) = Zrem a b.
-Proof.
- intros [|a|a] [|b|b]; trivial; unfold Zrem; simpl;
-  destruct N.pos_div_eucl; simpl; try rewrite Zopp_involutive; trivial.
-Qed.
+Notation Zquotrem_eq := Z.quotrem_eq (only parsing).
+Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
+Notation Zrem_bound := Z.rem_bound_pos (only parsing).
+Notation Zrem_opp_l := Z.rem_opp_l' (only parsing).
+Notation Zrem_opp_r := Z.rem_opp_r' (only parsing).
diff --git a/theories/ZArith/Zeuclid.v b/theories/ZArith/Zeuclid.v
index ece227e10..cd46ea36b 100644
--- a/theories/ZArith/Zeuclid.v
+++ b/theories/ZArith/Zeuclid.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Morphisms BinInt Zdiv_def ZBinary ZDivEucl.
+Require Import Morphisms BinInt Zdiv_def ZDivEucl.
 Local Open Scope Z_scope.
 
 (** * Definitions of division for binary integers, Euclid convention. *)
@@ -45,8 +45,8 @@ Module ZEuclid.
 
  Lemma mod_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= modulo a b < b.
  Proof.
-  intros a b _ Hb. rewrite <- (Z.abs_eq b) at 3 by z_order.
-  apply mod_always_pos. z_order.
+  intros a b _ Hb. rewrite <- (Z.abs_eq b) at 3 by Z.order.
+  apply mod_always_pos. Z.order.
  Qed.
 
  Include ZEuclidProp Z Z Z.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 9bff641b7..ef91f2d77 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -33,21 +33,8 @@ Definition Zodd (z:Z) :=
     | _ => False
   end.
 
-Definition Zeven_bool (z:Z) :=
-  match z with
-    | Z0 => true
-    | Zpos (xO _) => true
-    | Zneg (xO _) => true
-    | _ => false
-  end.
-
-Definition Zodd_bool (z:Z) :=
-  match z with
-    | Z0 => false
-    | Zpos (xO _) => false
-    | Zneg (xO _) => false
-    | _ => true
-  end.
+Notation Zeven_bool := Z.even (only parsing).
+Notation Zodd_bool := Z.odd (only parsing).
 
 Lemma Zeven_bool_iff : forall n, Zeven_bool n = true <-> Zeven n.
 Proof.
@@ -173,32 +160,8 @@ Qed.
 (** * Definition of [Zquot2], [Zdiv2] and properties wrt [Zeven]
   and [Zodd] *)
 
-(** [Zdiv2] performs rounding toward bottom, it is hence a particular
-   case of [Zdiv], and for all relative number [n] we have:
-   [n = 2 * Zdiv2 n + if Zodd_bool n then 1 else 0].  *)
-
-Definition Zdiv2 z :=
- match z with
-   | 0 => 0
-   | Zpos 1 => 0
-   | Zpos p => Zpos (Pdiv2 p)
-   | Zneg p => Zneg (Pdiv2_up p)
- end.
-
-(** [Zquot2] performs rounding toward zero, it is hence a particular
-   case of [Zquot], and for all relative number [n] we have:
-   [n = 2 * Zdiv2 n + if Zodd_bool n then Zsgn n else 0].  *)
-
-Definition Zquot2 (z:Z) :=
-  match z with
-    | 0 => 0
-    | Zpos 1 => 0
-    | Zpos p => Zpos (Pdiv2 p)
-    | Zneg 1 => 0
-    | Zneg p => Zneg (Pdiv2 p)
-  end.
-
-(** NB: [Zquot2] used to be named [Zdiv2] in Coq <= 8.3 *)
+Notation Zdiv2 := Z.div2 (only parsing).
+Notation Zquot2 := Z.quot2 (only parsing).
 
 (** Properties of [Zdiv2] *)
 
diff --git a/theories/ZArith/Zgcd_def.v b/theories/ZArith/Zgcd_def.v
index ad4c35eee..674f705e5 100644
--- a/theories/ZArith/Zgcd_def.v
+++ b/theories/ZArith/Zgcd_def.v
@@ -10,130 +10,12 @@ Require Import BinPos BinInt.
 
 Open Local Scope Z_scope.
 
-(** * Definition of a gcd function for relative numbers *)
-
-Definition Zgcd (a b : Z) : Z :=
-  match a,b with
-    | Z0, _ => Zabs b
-    | _, Z0 => Zabs a
-    | Zpos a, Zpos b => Zpos (Pos.gcd a b)
-    | Zpos a, Zneg b => Zpos (Pos.gcd a b)
-    | Zneg a, Zpos b => Zpos (Pos.gcd a b)
-    | Zneg a, Zneg b => Zpos (Pos.gcd a b)
-  end.
-
-(** * Generalized Gcd, also computing division of a and b by gcd. *)
-
-Definition Zggcd (a b : Z) : Z*(Z*Z) :=
-  match a,b with
-    | Z0, _ => (Zabs b,(Z0, Zsgn b))
-    | _, Z0 => (Zabs a,(Zsgn a, Z0))
-    | Zpos a, Zpos b =>
-       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zpos bb))
-    | Zpos a, Zneg b =>
-       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zneg bb))
-    | Zneg a, Zpos b =>
-       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zpos bb))
-    | Zneg a, Zneg b =>
-       let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zneg bb))
-  end.
-
-(** The first component of Zggcd is Zgcd *)
-
-Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b.
-Proof.
- intros [ |p|p] [ |q|q]; simpl; auto;
-  generalize (Pos.ggcd_gcd p q); destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence.
-Qed.
-
-(** The other components of Zggcd are indeed the correct factors. *)
-
-Lemma Zggcd_correct_divisors : forall a b,
-  let '(g,(aa,bb)) := Zggcd a b in
-  a = g*aa /\ b = g*bb.
-Proof.
- intros [ |p|p] [ |q|q]; simpl; rewrite ?Pmult_1_r; auto;
-  generalize (Pos.ggcd_correct_divisors p q);
-  destruct Pos.ggcd as (g,(aa,bb)); simpl; destruct 1; subst; auto.
-Qed.
-
-(** Divisibility. We use here a simple "exists", while the historical
-    Znumtheory.Zdivide is a specialized inductive type. *)
-
-Definition Zdivide' x y := exists z, x*z = y.
-
-Local Notation "( x | y )" := (Zdivide' x y) (at level 0).
-
-Lemma Zgcd_divide_l : forall a b, (Zgcd a b | a).
-Proof.
- intros a b. rewrite <- Zggcd_gcd. generalize (Zggcd_correct_divisors a b).
- destruct Zggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto.
-Qed.
-
-Lemma Zgcd_divide_r : forall a b, (Zgcd a b | b).
-Proof.
- intros a b. rewrite <- Zggcd_gcd. generalize (Zggcd_correct_divisors a b).
- destruct Zggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto.
-Qed.
-
-Lemma Zdivide'_0_l : forall x, (0|x) -> x = 0.
-Proof.
- intros x (y,H). auto.
-Qed.
-
-Lemma Zdivide'_Zpos_Zneg_r : forall x y, (x|Zpos y) <-> (x|Zneg y).
-Proof.
- intros x y; split; intros (z,H); exists (-z);
-  now rewrite <- Zopp_mult_distr_r, H.
-Qed.
-
-Lemma Zdivide'_Zpos_Zneg_l : forall x y, (Zpos x|y) <-> (Zneg x|y).
-Proof.
- intros x y; split; intros (z,H); exists (-z);
-  now rewrite <- Zmult_opp_comm.
-Qed.
-
-Lemma Zdivide'_Pdivide : forall p q, (Zpos p|Zpos q) <-> (p|q)%positive.
-Proof.
- intros p q. split.
- intros ([ |r|r],H); simpl in *; discriminate H || injection H. exists r; auto.
- intros (r,H). exists (Zpos r); simpl; f_equal; auto.
-Qed.
-
-Lemma Zgcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|Zgcd a b).
-Proof.
- assert (D : forall p q c, (c|Zpos p) -> (c|Zpos q) -> (c|Zpos (Pos.gcd p q))).
-  intros p q [|r|r] H H'.
-  apply Zdivide'_0_l in H. discriminate.
-  apply Zdivide'_Pdivide, Pos.gcd_greatest; now apply Zdivide'_Pdivide.
-  apply Zdivide'_Zpos_Zneg_l, Zdivide'_Pdivide, Pos.gcd_greatest;
-   now apply Zdivide'_Pdivide, Zdivide'_Zpos_Zneg_l.
- intros [ |p|p] [ |q|q]; simpl; auto; intros; try apply D; trivial;
-  now apply Zdivide'_Zpos_Zneg_r.
-Qed.
-
-Lemma Zgcd_nonneg : forall a b, 0 <= Zgcd a b.
-Proof.
- intros [ |p|p] [ |q|q]; discriminate.
-Qed.
-
-(*
-(** Zggcd produces coefficients that are relatively prime *)
-
-Lemma Zggcd_greatest : forall a b,
- let (aa,bb) := snd (Zggcd a b) in
- forall z, (z|aa) -> (z|bb) -> z=1 \/ z=-1.
-Proof.
- intros [ |p|p] [ |q|q]; simpl.
-*)
-
-
-(** Zggcd and opp : an auxiliary result used in QArith *)
-
-Theorem Zggcd_opp: forall x y,
-  Zggcd (-x) y = let '(g,(aa,bb)) := Zggcd x y in
-                 (g,(-aa,bb)).
-Proof.
-intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto;
- destruct (Pos.ggcd x y) as (g,(aa,bb)); auto.
-Qed.
+Notation Zgcd := Z.gcd (only parsing).
+Notation Zggcd := Z.ggcd (only parsing).
+Notation Zggcd_gcd := Z.ggcd_gcd (only parsing).
+Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing).
+Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing).
+Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing).
+Notation Zgcd_greatest := Z.gcd_greatest (only parsing).
+Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing).
+Notation Zggcd_opp := Z.ggcd_opp (only parsing).
diff --git a/theories/ZArith/Zlog_def.v b/theories/ZArith/Zlog_def.v
index 44983f691..8326cb13c 100644
--- a/theories/ZArith/Zlog_def.v
+++ b/theories/ZArith/Zlog_def.v
@@ -8,31 +8,6 @@
 
 Require Import BinInt Zorder Zpow_def.
 
-Local Open Scope Z_scope.
-
-(** Definition of Zlog2 *)
-
-Definition Zlog2 z :=
-  match z with
-    | Zpos (p~1) => Zpos (Psize_pos p)
-    | Zpos (p~0) => Zpos (Psize_pos p)
-    | _ => 0
-  end.
-
-Lemma Zlog2_spec : forall n, 0 < n ->
- 2^(Zlog2 n) <= n < 2^(Zsucc (Zlog2 n)).
-Proof.
- intros [|[p|p|]|] Hn; split; try easy; unfold Zlog2;
-  rewrite <- ?Zpos_succ_morphism, Zpower_Ppow.
- eapply Zle_trans with (Zpos (p~0)).
- apply Psize_pos_le.
- apply Zlt_le_weak. exact (Pcompare_p_Sp (p~0)).
- apply Psize_pos_gt.
- apply Psize_pos_le.
- apply Psize_pos_gt.
-Qed.
-
-Lemma Zlog2_nonpos : forall n, n<=0 -> Zlog2 n = 0.
-Proof.
- intros [|p|p] H; trivial; now destruct H.
-Qed.
+Notation Zlog2 := Z.log2 (only parsing).
+Notation Zlog2_spec := Z.log2_spec (only parsing).
+Notation Zlog2_nonpos := Z.log2_nonpos (only parsing).
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 375646bbd..a4b5390e3 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -5,9 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *)
 
-Require Export BinInt Zcompare Zorder ZBinary.
+(** THIS FILE IS DEPRECATED. *)
+
+Require Export BinInt Zcompare Zorder.
 
 Open Local Scope Z_scope.
 
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 98aea6d20..1f2de0c9f 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -5,9 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *)
 
-Require Import BinInt Zcompare Zorder ZBinary.
+(** THIS FILE IS DEPRECATED. *)
+
+Require Import BinInt Zcompare Zorder.
 
 Open Local Scope Z_scope.
 
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index 63317d9cb..8908175f6 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Orders BinInt Zcompare Zorder ZBinary.
+Require Import Orders BinInt Zcompare Zorder.
 
-(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *)
+(** THIS FILE IS DEPRECATED. *)
 
 (*begin hide*)
 (* Compatibility with names of the old Zminmax file *)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index f6b038cbd..6f512e4f3 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -18,16 +18,11 @@ Open Local Scope Z_scope.
 
 (** [n]th iteration of the function [f] *)
 
-Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) :=
-  match n with
-    | Z0 => x
-    | Zpos p => iter_pos p A f x
-    | Zneg p => x
-  end.
+Notation iter := @Z.iter (only parsing).
 
 Lemma iter_nat_of_Z : forall n A f x, 0 <= n ->
   iter n A f x = iter_nat (Zabs_nat n) A f x.
 intros n A f x; case n; auto.
-intros p _; unfold iter, Zabs_nat; apply iter_nat_of_P.
+intros p _; unfold Z.iter, Zabs_nat; apply iter_nat_of_P.
 intros p abs; case abs; trivial.
 Qed.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 24fdb3143..b9788de8b 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -37,7 +37,7 @@ Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.
 
 (** Results concerning divisibility*)
 
-Lemma Zdivide_equiv : forall a b, Zdivide' a b <-> Zdivide a b.
+Lemma Zdivide_equiv : forall a b, Z.divide a b <-> Zdivide a b.
 Proof.
  intros a b; split; intros (c,H); exists c; rewrite Zmult_comm; auto.
 Qed.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 1bd833d6f..fcac8c33a 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -444,10 +444,7 @@ Proof.
     [ assumption | apply Zgt_succ ].
 Qed.
 
-Lemma Zlt_succ_r : forall n m, n < Zsucc m <-> n <= m.
-Proof.
-  split; [apply Zlt_succ_le | apply Zle_lt_succ].
-Qed.
+Notation Zlt_succ_r := Z.lt_succ_r (only parsing).
 
 Lemma Zle_succ_l : forall n m, Zsucc n <= m <-> n < m.
 Proof.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
index 7121393bc..8307f7601 100644
--- a/theories/ZArith/Zpow_def.v
+++ b/theories/ZArith/Zpow_def.v
@@ -13,32 +13,11 @@ Local Open Scope Z_scope.
 (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
       integer (type [positive]) and [z] a signed integer (type [Z]) *)
 
-Definition Zpower_pos (z:Z) (n:positive) :=
- iter_pos n Z (fun x:Z => z * x) 1.
-
-Definition Zpower (x y:Z) :=
-    match y with
-      | Zpos p => Zpower_pos x p
-      | Z0 => 1
-      | Zneg p => 0
-    end.
-
-Infix "^" := Zpower : Z_scope.
-
-Lemma Zpower_0_r : forall n, n^0 = 1.
-Proof. reflexivity. Qed.
-
-Lemma Zpower_succ_r : forall a b, 0<=b -> a^(Zsucc b) = a * a^b.
-Proof.
- intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
- reflexivity.
- unfold Zpower_pos. now rewrite Pplus_comm, iter_pos_plus.
-Qed.
-
-Lemma Zpower_neg_r : forall a b, b<0 -> a^b = 0.
-Proof.
- now destruct b.
-Qed.
+Notation Zpower_pos := Z.pow_pos (only parsing).
+Notation Zpower := Z.pow (only parsing).
+Notation Zpower_0_r := Z.pow_0_r (only parsing).
+Notation Zpower_succ_r := Z.pow_succ_r (only parsing).
+Notation Zpower_neg_r := Z.pow_neg_r (only parsing).
 
 Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
 Proof.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 7c603c14d..d9c5f995b 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -181,16 +181,16 @@ Theorem Zpower_le_monotone2:
    forall a b c, 0 < a -> b <= c -> a^b <= a^c.
 Proof.
   intros a b c H H2.
-  destruct (Z_le_gt_dec 0 b).
+  destruct (Z_le_gt_dec 0 b) as [Hb|Hb].
   apply Zpower_le_monotone; auto.
   replace (a^b) with 0.
-  destruct (Z_le_gt_dec 0 c).
-  destruct (Zle_lt_or_eq _ _ z0).
+  destruct (Z_le_gt_dec 0 c) as [Hc|Hc].
+  destruct (Zle_lt_or_eq _ _ Hc) as [Hc'|Hc'].
   apply Zlt_le_weak;apply Zpower_gt_0;trivial.
-  rewrite <- H0;simpl;auto with zarith.
+  rewrite <- Hc';simpl;auto with zarith.
   replace (a^c) with 0. auto with zarith.
-  destruct c;trivial;unfold Zgt in z0;discriminate z0.
-  destruct b;trivial;unfold Zgt in z;discriminate z.
+  destruct c;trivial;unfold Zgt in Hc;discriminate Hc.
+  destruct b;trivial;unfold Zgt in Hb;discriminate Hb.
 Qed.
 
 Theorem Zmult_power: forall p q r, 0 <= r ->
@@ -225,10 +225,10 @@ Proof.
    apply Zpower_le_monotone;auto with zarith.
    apply Zpower_le_monotone3;auto with zarith.
   assert (c > 0).
-  destruct (Z_le_gt_dec 0 c);trivial.
-  destruct (Zle_lt_or_eq _ _ z0);auto with zarith.
+  destruct (Z_le_gt_dec 0 c) as [Hc|Hc];trivial.
+  destruct (Zle_lt_or_eq _ _ Hc);auto with zarith.
   rewrite <- H3 in H1;simpl in H1; exfalso;omega.
-  destruct c;try discriminate z0. simpl in H1. exfalso;omega.
+  destruct c;try discriminate Hc. simpl in H1. exfalso;omega.
   assert (H4 := Zpower_lt_monotone a c b H). exfalso;omega.
 Qed.
 
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index ae8c20875..b8b780831 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms Zdiv.
-Require Export Zdiv_def.
-Require ZBinary ZDivTrunc.
+Require Import Nnat ZArith_base ROmega ZArithRing Zdiv_def Zdiv Morphisms.
 
 Local Open Scope Z_scope.
 
@@ -94,7 +92,7 @@ Proof.
   assert (0 <= Zrem a b).
    generalize (Zrem_sgn a b).
    destruct (Zle_lt_or_eq 0 a H).
-   rewrite <- Zsgn_pos in H1; rewrite H1; romega with *.
+   rewrite <- Zsgn_pos in H1; rewrite H1. romega with *.
    subst a; simpl; auto.
   generalize (Zrem_lt a b H0); romega with *.
 Qed.
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index ce46aa6d4..1533eb925 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -221,9 +221,9 @@ Proof.
 Qed.
 
 
-(** Equivalence between Zsqrt_plain and [Zsqrt_def.Zsqrt] *)
+(** Equivalence between Zsqrt_plain and [Z.sqrt] *)
 
-Lemma Zsqrt_equiv : forall n, Zsqrt_plain n = Zsqrt_def.Zsqrt n.
+Lemma Zsqrt_equiv : forall n, Zsqrt_plain n = Z.sqrt n.
 Proof.
  intros. destruct (Z_le_gt_dec 0 n).
  symmetry. apply Z.sqrt_unique; trivial.
diff --git a/theories/ZArith/Zsqrt_def.v b/theories/ZArith/Zsqrt_def.v
index b3d1fa1eb..2012e8bcc 100644
--- a/theories/ZArith/Zsqrt_def.v
+++ b/theories/ZArith/Zsqrt_def.v
@@ -10,51 +10,9 @@
 
 Require Import BinPos BinInt.
 
-Local Open Scope Z_scope.
-
-Definition Zsqrtrem n :=
- match n with
-  | 0 => (0, 0)
-  | Zpos p =>
-    match Pos.sqrtrem p with
-     | (s, IsPos r) => (Zpos s, Zpos r)
-     | (s, _) => (Zpos s, 0)
-    end
-  | Zneg _ => (0,0)
- end.
-
-Definition Zsqrt n :=
- match n with
-  | 0 => 0
-  | Zpos p => Zpos (Pos.sqrt p)
-  | Zneg _ => 0
- end.
-
-Lemma Zsqrtrem_spec : forall n, 0<=n ->
- let (s,r) := Zsqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
-Proof.
- destruct n. now repeat split.
- generalize (Pos.sqrtrem_spec p). simpl.
- destruct 1; simpl; subst; now repeat split.
- now destruct 1.
-Qed.
-
-Lemma Zsqrt_spec : forall n, 0<=n ->
- let s := Zsqrt n in s*s <= n < (Zsucc s)*(Zsucc s).
-Proof.
- destruct n. now repeat split. unfold Zsqrt.
- rewrite <- Zpos_succ_morphism. intros _. apply (Pos.sqrt_spec p).
- now destruct 1.
-Qed.
-
-Lemma Zsqrt_neg : forall n, n<0 -> Zsqrt n = 0.
-Proof.
- intros. now destruct n.
-Qed.
-
-Lemma Zsqrtrem_sqrt : forall n, fst (Zsqrtrem n) = Zsqrt n.
-Proof.
- destruct n; try reflexivity.
- unfold Zsqrtrem, Zsqrt, Pos.sqrt.
- destruct (Pos.sqrtrem p) as (s,r). now destruct r.
-Qed.
\ No newline at end of file
+Notation Zsqrtrem := Z.sqrtrem (only parsing).
+Notation Zsqrt := Z.sqrt (only parsing).
+Notation Zsqrtrem_spec := Z.sqrtrem_spec (only parsing).
+Notation Zsqrt_spec := Z.sqrt_spec (only parsing).
+Notation Zsqrt_neg := Z.sqrt_neg (only parsing).
+Notation Zsqrtrem_sqrt := Z.sqrtrem_sqrt (only parsing).
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 8dc8e9276..cf0cdd7c7 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -1,4 +1,5 @@
 auxiliary.vo
+BinIntDef.vo
 BinInt.vo
 Int.vo
 Wf_Z.vo