Enhance the BigN and BigZ infrastructure:

 * Isolate and put forward the interfaces NSig and ZSig that describe
   what should contain structures of natural numbers and integers (specs 
   are done by translation to ZArith).

 * Functors NSigNAxioms and ZSigZAxioms proving that these NSig and 
   ZSig implements the fully-abstract NAxioms and ZAxioms module types.
   
 * BigN and BigZ now contains more notations, plus an export of all 
   abstract results proved by Evgeny instantiated thanks to NSigNAxioms
   and ZSigZAxioms. In addition, BigN and BigZ are declared as 
   (semi/full)-rings.

 * as a consequence, some incompatibities have to be fixed in BigQ: 
   - take care of some name masking (via Import, Open Scope ...)
   - some additionnal constants like BigN.lt to deal with



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

15 files changed, 1111 insertions, 525 deletions

diff --git a/Makefile.common b/Makefile.common
index c968b41b8..0053dafdc 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -685,10 +685,14 @@ NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \
 NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \
  NBinDefs.vo 	NBinary.vo )
 
+NATURALSPECVIAZVO:=$(addprefix theories/Numbers/Natural/SpecViaZ/, \
+ NSig.vo	NSigNAxioms.vo )
+
 NATURALBIGNVO:=$(addprefix theories/Numbers/Natural/BigN/, \
- Nbasic.vo 	NMake.vo 	BigN.vo 	NBigN.vo )
+ Nbasic.vo 	NMake.vo 	BigN.vo )
 
-NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) $(NATURALBIGNVO)
+NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \
+ $(NATURALSPECVIAZVO) $(NATURALBIGNVO)
 
 INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \
  ZAxioms.vo 	ZBase.vo 	ZPlus.vo 	ZTimes.vo 	\
@@ -700,11 +704,14 @@ INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \
 INTEGERNATPAIRSVO:=$(addprefix theories/Numbers/Integer/NatPairs/, \
  ZNatPairs.vo )
 
+INTEGERSPECVIAZVO:=$(addprefix theories/Numbers/Integer/SpecViaZ/, \
+ ZSig.vo	ZSigZAxioms.vo )
+
 INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \
  ZMake.vo 	BigZ.vo )
 
 INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \
- $(INTEGERBIGZVO)
+ $(INTEGERSPECVIAZVO) $(INTEGERBIGZVO)
 
 RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \
  QMake_base.vo	QpMake.vo	QvMake.vo	Q0Make.vo 	\
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 934fbc428..d2f9b0a02 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -11,50 +11,99 @@
 (*i $Id$ i*)
 
 Require Export BigN.
+Require Import ZTimesOrder.
+Require Import ZSig.
+Require Import ZSigZAxioms.
 Require Import ZMake.
 
+Module BigZ <: ZType := ZMake.Make BigN.
 
-Module BigZ := Make BigN.
+(** Module [BigZ] implements [ZAxiomsSig] *)
 
+Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
+Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod.
 
-Definition bigZ := BigZ.t.
+(** Notations about [BigZ] *)
+
+Notation bigZ := BigZ.t.
 
 Delimit Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
 
-Notation " i + j " := (BigZ.add i j) : bigZ_scope.
-Notation " i - j " := (BigZ.sub i j) : bigZ_scope.
-Notation " i * j " := (BigZ.mul i j) : bigZ_scope.
-Notation " i / j " := (BigZ.div i j) : bigZ_scope.
-Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope.
-
-
- Theorem spec_to_Z: 
-  forall n, BigN.to_Z (BigZ.to_N n) = 
-            (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_N n: 
-  (BigZ.to_Z n = 
-    Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_Z_pos: 
-  forall n, (0 <= BigZ.to_Z n ->
-              BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 _  H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
+Notation Local "0" := BigZ.zero : bigZ_scope.
+Infix "+" := BigZ.add : bigZ_scope.
+Infix "-" := BigZ.sub : bigZ_scope.
+Notation "- x" := (BigZ.opp x) : bigZ_scope.
+Infix "*" := BigZ.mul : bigZ_scope.
+Infix "/" := BigZ.div : bigZ_scope.
+Infix "?=" := BigZ.compare : bigZ_scope.
+Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
+Infix "<" := BigZ.lt : bigZ_scope.
+Infix "<=" := BigZ.le : bigZ_scope.
+Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
+
+Open Scope bigZ_scope.
+
+(** Some additional results about [BigZ] *)
+
+Theorem spec_to_Z: forall n:bigZ, 
+  BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Theorem spec_to_N n: 
+ ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
+  BigN.to_Z (BigZ.to_N n) = [n].
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 _ H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Lemma sub_opp : forall x y : bigZ, x - y == x + (- y).
+Proof.
+red; intros; zsimpl; auto.
+Qed.
+
+Lemma plus_opp : forall x : bigZ, x + (- x) == 0.
+Proof.
+red; intros; zsimpl; auto with zarith.
+Qed.
+
+(** [BigZ] is a ring *)
+
+Lemma BigZring : 
+ ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
+Proof.
+constructor.
+exact Zplus_0_l.
+exact Zplus_comm.
+exact Zplus_assoc.
+exact Ztimes_1_l.
+exact Ztimes_comm.
+exact Ztimes_assoc.
+exact Ztimes_plus_distr_r.
+exact sub_opp.
+exact plus_opp.
+Qed.
+
+Add Ring BigZr : BigZring.
+
+(** Todo: tactic translating from [BigZ] to [Z] + omega *)
 
+(** Todo: micromega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 83171388d..cbf6f701f 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -12,94 +12,18 @@
 
 Require Import ZArith.
 Require Import BigNumPrelude.
+Require Import NSig.
+Require Import ZSig.
 
 Open Scope Z_scope.
 
-Module Type NType.
-
- Parameter t : Type.
- 
- Parameter zero : t.
- Parameter one : t.
-
- Parameter of_N : N -> t.
- Parameter to_Z : t -> Z.
- Parameter spec_pos: forall x, 0 <= to_Z x.
- Parameter spec_0: to_Z zero = 0.
- Parameter spec_1: to_Z one = 1.
- Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x.
-
- Parameter compare : t -> t -> comparison.
-
- Parameter spec_compare: forall x y,
-    match compare x y with
-      Eq => to_Z x = to_Z y
-    | Lt => to_Z x < to_Z y
-    | Gt => to_Z x > to_Z y
-    end.
-
- Parameter eq_bool : t -> t -> bool.
-
- Parameter spec_eq_bool: forall x y,
-    if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y.
- 
- Parameter succ : t -> t.
-
- Parameter spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
-
- Parameter add  : t -> t -> t.
-
- Parameter spec_add: forall x y, to_Z (add x y) = to_Z x +  to_Z y.
-
- Parameter pred : t -> t.
-
- Parameter spec_pred: forall x, 0 < to_Z x -> to_Z (pred x) = to_Z x - 1.
-
- Parameter sub  : t -> t -> t.
-
- Parameter spec_sub: forall x y, to_Z y <= to_Z x ->
-   to_Z (sub x y) = to_Z x - to_Z y.
-
- Parameter mul       : t -> t -> t.
-
- Parameter spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.
-
- Parameter square    : t -> t.
-
- Parameter spec_square: forall x, to_Z (square x) = to_Z x *  to_Z x.
-
- Parameter power_pos : t -> positive -> t.
-
- Parameter spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
-
- Parameter sqrt      : t -> t.
-
- Parameter spec_sqrt: forall x, to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
-
- Parameter div_eucl : t -> t -> t * t.
-
- Parameter spec_div_eucl: forall x y,
-      0 < to_Z y ->
-      let (q,r) := div_eucl x y in (to_Z q, to_Z r) = (Zdiv_eucl (to_Z x) (to_Z y)).
+(** * ZMake 
  
- Parameter div      : t -> t -> t.
-
- Parameter spec_div: forall x y,
-      0 < to_Z y -> to_Z (div x y) = to_Z x / to_Z y.
-
- Parameter modulo   : t -> t -> t.
-
- Parameter spec_modulo:
-   forall x y, 0 < to_Z y -> to_Z (modulo x y) = to_Z x mod to_Z y.
-
- Parameter gcd      : t -> t -> t.
-
- Parameter spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
-
-
-End NType.
+  A generic transformation from a structure of natural numbers 
+  [NSig.NType] to a structure of integers [ZSig.ZType].
+*)
 
-Module Make (N:NType).
+Module Make (N:NType) <: ZType.
  
  Inductive t_ := 
   | Pos : N.t -> t_
@@ -131,6 +55,7 @@ Module Make (N:NType).
    intros; rewrite N.spec_of_N; auto.
  Qed.
 
+ Definition eq x y := (to_Z x = to_Z y).
 
  Theorem spec_0: to_Z zero = 0.
  exact N.spec_0.
@@ -160,6 +85,10 @@ Module Make (N:NType).
   | Neg nx, Neg ny => N.compare ny nx
   end.
 
+ Definition lt n m := compare n m = Lt.
+ Definition le n m := compare n m <> Gt.
+ Definition min n m := match compare n m with Gt => m | _ => n end.
+ Definition max n m := match compare n m with Lt => m | _ => n end.
 
  Theorem spec_compare: forall x y,
     match compare x y with
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
new file mode 100644
index 000000000..4e4593983
--- /dev/null
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -0,0 +1,117 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith Znumtheory.
+
+Open Scope Z_scope.
+
+(** * ZSig *)
+
+(** Interface of a rich structure about integers.
+    Specifications are written via translation to Z.
+*)
+
+Module Type ZType.
+
+ Parameter t : Type.
+
+ Parameter to_Z : t -> Z.
+ Notation "[ x ]" := (to_Z x).
+
+ Definition eq x y := ([x] = [y]).
+
+ Parameter of_Z : Z -> t.
+ Parameter spec_of_Z: forall x, to_Z (of_Z x) = x.
+
+ Parameter zero : t.
+ Parameter one : t.
+ Parameter minus_one : t.
+
+ Parameter spec_0: [zero] = 0.
+ Parameter spec_1: [one] = 1.
+ Parameter spec_m1: [minus_one] = -1.
+
+ Parameter compare : t -> t -> comparison.
+
+ Parameter spec_compare: forall x y,
+   match compare x y with
+     | Eq => [x] = [y]
+     | Lt => [x] < [y]
+     | Gt => [x] > [y]
+   end.
+
+ Definition lt n m := compare n m = Lt.
+ Definition le n m := compare n m <> Gt.
+ Definition min n m := match compare n m with Gt => m | _ => n end.
+ Definition max n m := match compare n m with Lt => m | _ => n end.
+
+ Parameter eq_bool : t -> t -> bool.
+
+ Parameter spec_eq_bool: forall x y,
+    if eq_bool x y then [x] = [y] else [x] <> [y].
+ 
+ Parameter succ : t -> t.
+
+ Parameter spec_succ: forall n, [succ n] = [n] + 1.
+
+ Parameter add  : t -> t -> t.
+
+ Parameter spec_add: forall x y, [add x y] = [x] + [y].
+
+ Parameter pred : t -> t.
+
+ Parameter spec_pred: forall x, [pred x] = [x] - 1.
+
+ Parameter sub : t -> t -> t.
+
+ Parameter spec_sub: forall x y, [sub x y] = [x] - [y].
+
+ Parameter opp : t -> t.
+
+ Parameter spec_opp: forall x, [opp x] = - [x].
+
+ Parameter mul : t -> t -> t.
+
+ Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
+
+ Parameter square : t -> t.
+
+ Parameter spec_square: forall x, [square x] = [x] *  [x].
+
+ Parameter power_pos : t -> positive -> t.
+
+ Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+
+ Parameter sqrt : t -> t.
+
+ Parameter spec_sqrt: forall x, 0 <= [x] -> 
+   [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
+
+ Parameter div_eucl : t -> t -> t * t.
+
+ Parameter spec_div_eucl: forall x y, [y] <> 0 ->
+   let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+ 
+ Parameter div : t -> t -> t.
+
+ Parameter spec_div: forall x y, [y] <> 0 -> [div x y] = [x] / [y].
+
+ Parameter modulo : t -> t -> t.
+
+ Parameter spec_modulo: forall x y, [y] <> 0 -> 
+   [modulo x y] = [x] mod [y].
+
+ Parameter gcd : t -> t -> t.
+
+ Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b).
+
+End ZType.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
new file mode 100644
index 000000000..3d9d3d190
--- /dev/null
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -0,0 +1,306 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith.
+Require Import ZAxioms.
+Require Import ZSig.
+
+(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
+
+Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.t.
+Open Local Scope IntScope.
+Notation "[ x ]" := (Z.to_Z x) : IntScope.
+Infix "=="  := Z.eq (at level 70) : IntScope.
+Notation "0" := Z.zero : IntScope.
+Infix "+" := Z.add : IntScope.
+Infix "-" := Z.sub : IntScope.
+Infix "*" := Z.mul : IntScope.
+Notation "- x" := (Z.opp x) : IntScope.
+
+Hint Rewrite 
+ Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
+ Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec.
+
+Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec.
+
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ := Z.t.
+Definition NZeq := Z.eq.
+Definition NZ0 := Z.zero.
+Definition NZsucc := Z.succ.
+Definition NZpred := Z.pred.
+Definition NZplus := Z.add.
+Definition NZminus := Z.sub.
+Definition NZtimes := Z.mul.
+
+Theorem NZeq_equiv : equiv Z.t Z.eq.
+Proof.
+repeat split; repeat red; intros; auto; congruence.
+Qed.
+
+Add Relation Z.t Z.eq
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+ as NZeq_rel.
+
+Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZplus with signature Z.eq ==> Z.eq ==> Z.eq as NZplus_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZtimes with signature Z.eq ==> Z.eq ==> Z.eq as NZtimes_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Section Induction.
+
+Variable A : Z.t -> Prop.
+Hypothesis A_wd : predicate_wd Z.eq A.
+Hypothesis A0 : A 0.
+Hypothesis AS : forall n, A n <-> A (Z.succ n). 
+
+Add Morphism A with signature Z.eq ==> iff as A_morph.
+Proof. apply A_wd. Qed.
+
+Let B (z : Z) := A (Z.of_Z z).
+
+Lemma B0 : B 0.
+Proof.
+unfold B; simpl.
+rewrite <- (A_wd 0); auto.
+zsimpl; auto.
+Qed.
+
+Lemma BS : forall z : Z, B z -> B (z + 1).
+Proof.
+intros z H.
+unfold B in *. apply -> AS in H.
+setoid_replace (Z.of_Z (z + 1)) with (Z.succ (Z.of_Z z)); auto.
+zsimpl; auto.
+Qed.
+
+Lemma BP : forall z : Z, B z -> B (z - 1).
+Proof.
+intros z H.
+unfold B in *. rewrite AS.
+setoid_replace (Z.succ (Z.of_Z (z - 1))) with (Z.of_Z z); auto.
+zsimpl; auto with zarith.
+Qed.
+
+Lemma B_holds : forall z : Z, B z.
+Proof.
+intros; destruct (Z_lt_le_dec 0 z).
+apply natlike_ind; auto with zarith.
+apply B0.
+intros; apply BS; auto.
+replace z with (-(-z))%Z in * by (auto with zarith).
+remember (-z)%Z as z'.
+pattern z'; apply natlike_ind.
+apply B0.
+intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto.
+subst z'; auto with zarith.
+Qed.
+
+Theorem NZinduction : forall n, A n.
+Proof.
+intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)).
+apply B_holds.
+zsimpl; auto.
+Qed.
+
+End Induction.
+
+Theorem NZplus_0_l : forall n, 0 + n == n.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZplus_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZminus_0_r : forall n, n - 0 == n.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZtimes_0_l : forall n, 0 * n == 0.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZtimes_succ_l : forall n m, (Z.succ n) * m == n * m + m.
+Proof.
+intros; zsimpl; ring.
+Qed.
+
+End NZAxiomsMod.
+
+Definition NZlt := Z.lt.
+Definition NZle := Z.le.
+Definition NZmin := Z.min.
+Definition NZmax := Z.max.
+
+Infix "<=" := Z.le : IntScope.
+Infix "<" := Z.lt : IntScope.
+
+Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z.
+Proof.
+ intros; generalize (Z.spec_compare x y).
+ destruct (Z.compare x y); auto.
+ intros H; rewrite H; symmetry; apply Zcompare_refl.
+Qed.
+
+Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
+Proof.
+ intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition.
+Qed.
+
+Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
+Proof.
+ intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition.
+Qed.
+
+Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y].
+Proof.
+ intros; unfold Z.min, Zmin.
+ rewrite spec_compare_alt; destruct Zcompare; auto.
+Qed.
+
+Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y].
+Proof.
+ intros; unfold Z.max, Zmax.
+ rewrite spec_compare_alt; destruct Zcompare; auto.
+Qed.
+
+Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd.
+Proof. 
+intros x x' Hx y y' Hy.
+rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd.
+Proof.
+intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd.
+Proof.
+intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd.
+Proof.
+intros; red; rewrite 2 spec_min; congruence.
+Qed.
+
+Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd.
+Proof.
+intros; red; rewrite 2 spec_max; congruence.
+Qed.
+
+Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Proof.
+intros.
+unfold Z.eq; rewrite spec_lt, spec_le; omega.
+Qed.
+
+Theorem NZlt_irrefl : forall n, ~ n < n.
+Proof.
+intros; rewrite spec_lt; auto with zarith.
+Qed.
+
+Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.
+Proof.
+intros; rewrite spec_lt, spec_le, Z.spec_succ; omega.
+Qed.
+
+Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_min.
+generalize (Zmin_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_min.
+generalize (Zmin_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_max.
+generalize (Zmax_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_max.
+generalize (Zmax_spec [n] [m]); omega.
+Qed.
+
+End NZOrdAxiomsMod.
+
+Definition Zopp := Z.opp.
+
+Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n.
+Proof.
+red; intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem Zopp_0 : - 0 == 0.
+Proof.
+red; intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n).
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+End ZSig_ZAxioms.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 033364f72..881b7984c 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -17,32 +17,67 @@ Author: Arnaud Spiwack
 Require Export Int31.
 Require Import CyclicAxioms.
 Require Import Cyclic31.
+Require Import NSig.
+Require Import NSigNAxioms.
 Require Import NMake.
+Require Import NMinus.
 
-Open Scope int31_scope.
+Module BigN <: NType := NMake.Make Int31Cyclic.
 
-Module BigN := NMake.Make Int31Cyclic.
+(** Module [BigN] implements [NAxiomsSig] *)
 
-Definition bigN := BigN.t.
+Module Export BigNAxiomsMod := NSig_NAxioms BigN.
+Module Export BigNMinusPropMod := NMinusPropFunct BigNAxiomsMod.
+
+(** Notations about [BigN] *)
+
+Notation bigN := BigN.t.
 
 Delimit Scope bigN_scope with bigN.
 Bind Scope bigN_scope with bigN.
 Bind Scope bigN_scope with BigN.t.
 Bind Scope bigN_scope with BigN.t_.
 
-Notation " i + j " := (BigN.add i j) : bigN_scope.
-Notation " i - j " := (BigN.sub i j) : bigN_scope.
-Notation " i * j " := (BigN.mul i j) : bigN_scope.
-Notation " i / j " := (BigN.div i j) : bigN_scope.
-Notation " i ?= j " := (BigN.compare i j) : bigN_scope.
-
- Theorem succ_pred: forall q,
-  (0 < BigN.to_Z q -> 
-     BigN.to_Z (BigN.succ (BigN.pred q)) = BigN.to_Z q)%Z.
- intros q Hq.
- rewrite BigN.spec_succ.
- rewrite BigN.spec_pred; auto.
- generalize Hq; set (a := BigN.to_Z q).
- ring_simplify (a - 1 + 1)%Z; auto.
- Qed.
- 
+Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *)
+Infix "+" := BigN.add : bigN_scope.
+Infix "-" := BigN.sub : bigN_scope.
+Infix "*" := BigN.mul : bigN_scope.
+Infix "/" := BigN.div : bigN_scope.
+Infix "?=" := BigN.compare : bigN_scope.
+Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
+Infix "<" := BigN.lt : bigN_scope.
+Infix "<=" := BigN.le : bigN_scope.
+Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
+
+Open Scope bigN_scope.
+
+(** Example of reasoning about [BigN] *)
+
+Theorem succ_pred: forall q:bigN,
+  0 < q -> BigN.succ (BigN.pred q) == q.
+Proof.
+intros; apply succ_pred.
+intro H'; rewrite H' in H; discriminate.
+Qed.
+
+(** [BigN] is a semi-ring *)
+
+Lemma BigNring : 
+ semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
+Proof.
+constructor.
+exact plus_0_l.
+exact plus_comm.
+exact plus_assoc.
+exact times_1_l.
+exact times_0_l.
+exact times_comm.
+exact times_assoc.
+exact times_plus_distr_r.
+Qed.
+
+Add Ring BigNr : BigNring.
+
+(** Todo: tactic translating from [BigN] to [Z] + omega *)
+
+(** Todo: micromega *)
diff --git a/theories/Numbers/Natural/BigN/NBigN.v b/theories/Numbers/Natural/BigN/NBigN.v
deleted file mode 100644
index e933b6578..000000000
--- a/theories/Numbers/Natural/BigN/NBigN.v
+++ /dev/null
@@ -1,364 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Import Nnat.
-Require Import NMinus.
-Require Export BigN.
-
-(** * [BigN] implements [NAxiomsSig] *)
-
-Module BigNAxiomsMod <: NAxiomsSig.
-Import BigN.
-Open Local Scope bigN_scope.
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
-
-Definition NZ := bigN.
-Definition NZeq n m := (to_Z n = to_Z m).
-Definition NZ0 := 0.
-Definition NZsucc := succ.
-Definition NZpred := pred.
-Definition NZplus := add.
-Definition NZminus := sub.
-Definition NZtimes := mul.
-
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with NZ.
-Open Local Scope IntScope.
-Notation "[ x ]" := (to_Z x).
-Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
-Notation "0" := NZ0 : IntScope.
-Notation "'S'" := NZsucc : IntScope.
-Notation "'P'" := NZpred : IntScope.
-Notation "x + y" := (NZplus x y) : IntScope.
-Notation "x - y" := (NZminus x y) : IntScope.
-Notation "x * y" := (NZtimes x y) : IntScope.
-
-Theorem NZeq_equiv : equiv NZ NZeq.
-Proof.
-unfold NZeq; repeat split; repeat red; intros; auto; congruence.
-Qed.
-
-Add Relation NZ NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
- as NZeq_rel.
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Proof.
-unfold NZeq; intros; rewrite 2 spec_succ; f_equal; auto.
-Qed.
-
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Proof.
-unfold NZeq; intros.
-generalize (spec_pos y) (spec_pos x) (spec_eq_bool x 0).
-destruct eq_bool; change (to_Z 0) with 0%Z; intros.
-rewrite 2 spec_pred0; congruence.
-rewrite 2 spec_pred; f_equal; auto; try omega.
-Qed.
-
-Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
-Proof.
-unfold NZeq; intros; rewrite 2 spec_add; f_equal; auto.
-Qed.
-
-Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
-Proof.
-unfold NZeq; intros x x' Hx y y' Hy.
-destruct (Z_lt_le_dec [x] [y]).
-rewrite 2 spec_sub0; f_equal; congruence.
-rewrite 2 spec_sub; f_equal; congruence.
-Qed.
-
-Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
-Proof.
-unfold NZeq; intros; rewrite 2 spec_mul; f_equal; auto.
-Qed.
-
-Theorem NZpred_succ : forall n : NZ, P (S n) == n.
-Proof.
-unfold NZeq; intros.
-rewrite BigN.spec_pred; rewrite BigN.spec_succ.
-omega.
-generalize (BigN.spec_pos n); omega.
-Qed.
-
-Definition of_Z z := of_N (Zabs_N z).
-
-Section Induction.
-
-Variable A : NZ -> Prop.
-Hypothesis A_wd : predicate_wd NZeq A.
-Hypothesis A0 : A 0.
-Hypothesis AS : forall n : NZ, A n <-> A (S n). 
-
-Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
-
-Let B (z : Z) := A (of_Z z).
-
-Lemma B0 : B 0.
-Proof.
-exact A0.
-Qed.
-
-Lemma BS : forall z : Z, 0 <= z -> B z -> B (z + 1).
-Proof.
-intros z H1 H2.
-unfold B in *. apply -> AS in H2.
-setoid_replace (of_Z (z + 1)) with (S (of_Z z)); auto.
-unfold NZeq. rewrite spec_succ.
-unfold of_Z.
-rewrite 2 spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith.
-Qed.
-
-Lemma B_holds : forall z : Z, 0 <= z -> B z.
-Proof.
-exact (natlike_ind B B0 BS).
-Qed.
-
-Theorem NZinduction : forall n : NZ, A n.
-Proof.
-intro n. setoid_replace n with (of_Z (to_Z n)).
-apply B_holds. apply spec_pos.
-red; unfold of_Z.
-rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto.
-apply spec_pos.
-Qed.
-
-End Induction.
-
-Theorem NZplus_0_l : forall n : NZ, 0 + n == n.
-Proof.
-intros; red; rewrite spec_add; auto with zarith.
-Qed.
-
-Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m).
-Proof.
-intros; red; rewrite spec_add, 2 spec_succ, spec_add; auto with zarith.
-Qed.
-
-Theorem NZminus_0_r : forall n : NZ, n - 0 == n.
-Proof.
-intros; red; rewrite spec_sub; change [0] with 0%Z; auto with zarith.
-apply spec_pos.
-Qed.
-
-Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m).
-Proof.
-intros; red.
-destruct (Z_lt_le_dec [n] [S m]) as [H|H].
-rewrite spec_sub0; auto.
-rewrite spec_succ in H.
-rewrite spec_pred0; auto.
-destruct (Z_eq_dec [n] [m]).
-rewrite spec_sub; auto with zarith.
-rewrite spec_sub0; auto with zarith.
-
-rewrite spec_sub, spec_succ in *; auto.
-rewrite spec_pred, spec_sub; auto with zarith.
-rewrite spec_sub; auto with zarith.
-Qed.
-
-Theorem NZtimes_0_l : forall n : NZ, 0 * n == 0.
-Proof.
-intros; red.
-rewrite spec_mul; auto with zarith.
-Qed.
-
-Theorem NZtimes_succ_l : forall n m : NZ, (S n) * m == n * m + m.
-Proof.
-intros; red.
-rewrite spec_add, 2 spec_mul, spec_succ; ring.
-Qed.
-
-End NZAxiomsMod.
-
-Open Scope bigN_scope.
-Open Scope IntScope.
-
-Definition NZlt n m := (compare n m = Lt).
-Definition NZle n m := (compare n m <> Gt).
-Definition NZmin n m := match compare n m with Gt => m | _ => n end.
-Definition NZmax n m := match compare n m with Lt => m | _ => n end.
-
-Infix "<=" := NZle : IntScope.
-Infix "<" := NZlt : IntScope.
-
-Lemma spec_compare_alt : forall x y, (x ?= y) = ([x] ?= [y])%Z.
-Proof.
- intros; generalize (spec_compare x y).
- destruct (x ?= y); auto.
- intros H; rewrite H; symmetry; apply Zcompare_refl.
-Qed.
-
-Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
-Proof.
- intros; unfold NZlt, Zlt; rewrite spec_compare_alt; intuition.
-Qed.
-
-Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
-Proof.
- intros; unfold NZle, Zle; rewrite spec_compare_alt; intuition.
-Qed.
-
-Lemma spec_min : forall x y, [NZmin x y] = Zmin [x] [y].
-Proof.
- intros; unfold NZmin, Zmin.
- rewrite spec_compare_alt; destruct Zcompare; auto.
-Qed.
-
-Lemma spec_max : forall x y, [NZmax x y] = Zmax [x] [y].
-Proof.
- intros; unfold NZmax, Zmax.
- rewrite spec_compare_alt; destruct Zcompare; auto.
-Qed.
-
-Add Morphism compare with signature NZeq ==> NZeq ==> (@eq comparison) as compare_wd.
-Proof. 
-intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
-Qed.
-
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-intros x x' Hx y y' Hy; unfold NZlt; rewrite Hx, Hy; intuition.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-intros x x' Hx y y' Hy; unfold NZle; rewrite Hx, Hy; intuition.
-Qed.
-
-Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
-Proof.
-intros; red; rewrite 2 spec_min; congruence.
-Qed.
-
-Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
-Proof.
-intros; red; rewrite 2 spec_max; congruence.
-Qed.
-
-Theorem NZlt_eq_cases : forall n m : NZ, n <= m <-> n < m \/ n == m.
-Proof.
-intros.
-unfold NZeq; rewrite spec_lt, spec_le; omega.
-Qed.
-
-Theorem NZlt_irrefl : forall n : NZ, ~ n < n.
-Proof.
-intros; rewrite spec_lt; auto with zarith.
-Qed.
-
-Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m.
-Proof.
-intros; rewrite spec_lt, spec_le, spec_succ; omega.
-Qed.
-
-Theorem NZmin_l : forall n m : NZ, n <= m -> NZmin n m == n.
-Proof.
-intros n m; unfold NZeq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
-Qed.
-
-Theorem NZmin_r : forall n m : NZ, m <= n -> NZmin n m == m.
-Proof.
-intros n m; unfold NZeq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
-Qed.
-
-Theorem NZmax_l : forall n m : NZ, m <= n -> NZmax n m == n.
-Proof.
-intros n m; unfold NZeq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
-Qed.
-
-Theorem NZmax_r : forall n m : NZ, n <= m -> NZmax n m == m.
-Proof.
-intros n m; unfold NZeq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
-Qed.
-
-End NZOrdAxiomsMod.
-
-Theorem pred_0 : P 0 == 0.
-Proof.
-reflexivity.
-Qed.
-
-Definition to_N n := Zabs_N (to_Z n).
-
-Definition recursion (A : Type) (a : A) (f : NZ -> A -> A) (n : NZ) :=
-  Nrect (fun _ => A) a (fun n a => f (of_N n) a) (to_N n).
-Implicit Arguments recursion [A].
-
-Theorem recursion_wd :
-forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : NZ -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
-      forall x x' : NZ, x == x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
-Proof.
-unfold fun2_wd, NZeq, fun2_eq.
-intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
-unfold recursion.
-unfold to_N.
-rewrite <- Exx'; clear x' Exx'.
-replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])).
-induction (Zabs_nat [x]).
-simpl; auto.
-rewrite N_of_S, 2 Nrect_step; auto.
-destruct [x]; simpl; auto.
-change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
-change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
-Qed.
-
-Theorem recursion_0 :
-  forall (A : Type) (a : A) (f : NZ -> A -> A), recursion a f 0 = a.
-Proof.
-intros A a f; unfold recursion; now rewrite Nrect_base.
-Qed.
-
-Theorem recursion_succ :
-  forall (A : Type) (Aeq : relation A) (a : A) (f : NZ -> A -> A),
-    Aeq a a -> fun2_wd NZeq Aeq Aeq f ->
-      forall n : NZ, Aeq (recursion a f (S n)) (f n (recursion a f n)).
-Proof.
-unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n.
-replace (to_N (S n)) with (Nsucc (to_N n)).
-rewrite Nrect_step.
-apply f_wd; auto.
-unfold to_N.
-rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto.
- apply spec_pos.
-
-fold (recursion a f n).
-apply recursion_wd; auto.
-red; auto.
-red; auto.
-unfold to_N.
-
-rewrite spec_succ.
-change ([n]+1)%Z with (Zsucc [n]).
-apply Z_of_N_eq_rev.
-rewrite Z_of_N_succ.
-rewrite 2 Z_of_N_abs.
-rewrite 2 Zabs_eq; auto.
-generalize (spec_pos n); auto with zarith.
-apply spec_pos; auto.
-Qed.
-
-End BigNAxiomsMod.
-
-Module Export BigNMinusPropMod := NMinusPropFunct BigNAxiomsMod.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 22a4b200a..534b680e2 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -79,8 +79,9 @@ let _ =
   pr "Require Import Nbasic.";
   pr "Require Import Wf_nat.";
   pr "Require Import StreamMemo.";
+  pr "Require Import NSig.";
   pr "";
-  pr "Module Make (Import W0:CyclicType).";
+  pr "Module Make (Import W0:CyclicType) <: NType.";
   pr "";
 
   pr " Definition w0 := W0.w.";
@@ -163,8 +164,13 @@ let _ =
 
   pr " Open Scope Z_scope.";
   pr " Notation \"[ x ]\" := (to_Z x).";
-  pr " ";
+  pr "";
 
+  pr " Definition to_N x := Zabs_N (to_Z x).";
+  pr "";
+  
+  pr " Definition eq x y := (to_Z x = to_Z y).";
+  pr "";
 
   pp " (* Regular make op (no karatsuba) *)";
   pp " Fixpoint nmake_op (ww:Type) (ww_op: znz_op ww) (n: nat) : ";
@@ -1315,6 +1321,12 @@ let _ =
   pr "      comparenm).";
   pr "";
 
+  pr " Definition lt n m := compare n m = Lt.";
+  pr " Definition le n m := compare n m <> Gt.";
+  pr " Definition min n m := match compare n m with Gt => m | _ => n end.";
+  pr " Definition max n m := match compare n m with Lt => m | _ => n end.";
+  pr "";
+
   for i = 0 to size do
     pp " Let spec_compare_%i: forall x y," i;
     pp "    match compare_%i x y with " i;
@@ -2396,7 +2408,6 @@ let _ =
   pr "  end.";
   pr "";
 
-
   pr " Theorem spec_of_N: forall x,";
   pr "   [of_N x] = Z_of_N x.";
   pa " Admitted.";
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
new file mode 100644
index 000000000..e53e627ec
--- /dev/null
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -0,0 +1,115 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith Znumtheory.
+
+Open Scope Z_scope.
+
+(** * NSig *)
+
+(** Interface of a rich structure about natural numbers.
+    Specifications are written via translation to Z.
+*)
+
+Module Type NType.
+
+ Parameter t : Type.
+
+ Parameter to_Z : t -> Z.
+ Notation "[ x ]" := (to_Z x).
+ Parameter spec_pos: forall x, 0 <= [x].
+
+ Parameter of_N : N -> t.
+ Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x.
+ Definition to_N n := Zabs_N (to_Z n).
+
+ Definition eq n m := ([n] = [m]).
+
+ Parameter zero : t.
+ Parameter one : t.
+
+ Parameter spec_0: [zero] = 0.
+ Parameter spec_1: [one] = 1.
+
+ Parameter compare : t -> t -> comparison.
+
+ Parameter spec_compare: forall x y,
+   match compare x y with
+     | Eq => [x] = [y]
+     | Lt => [x] < [y]
+     | Gt => [x] > [y]
+   end.
+
+ Definition lt n m := compare n m = Lt.
+ Definition le n m := compare n m <> Gt.
+ Definition min n m := match compare n m with Gt => m | _ => n end.
+ Definition max n m := match compare n m with Lt => m | _ => n end.
+
+ Parameter eq_bool : t -> t -> bool.
+
+ Parameter spec_eq_bool: forall x y,
+    if eq_bool x y then [x] = [y] else [x] <> [y].
+ 
+ Parameter succ : t -> t.
+
+ Parameter spec_succ: forall n, [succ n] = [n] + 1.
+
+ Parameter add  : t -> t -> t.
+
+ Parameter spec_add: forall x y, [add x y] = [x] + [y].
+
+ Parameter pred : t -> t.
+
+ Parameter spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.
+ Parameter spec_pred0: forall x, [x] = 0 -> [pred x] = 0.
+
+ Parameter sub : t -> t -> t.
+
+ Parameter spec_sub: forall x y, [y] <= [x] -> [sub x y] = [x] - [y].
+ Parameter spec_sub0: forall x y, [x] < [y]-> [sub x y] = 0.
+
+ Parameter mul : t -> t -> t.
+
+ Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
+
+ Parameter square : t -> t.
+
+ Parameter spec_square: forall x, [square x] = [x] *  [x].
+
+ Parameter power_pos : t -> positive -> t.
+
+ Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+
+ Parameter sqrt : t -> t.
+
+ Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
+
+ Parameter div_eucl : t -> t -> t * t.
+
+ Parameter spec_div_eucl: forall x y,
+      0 < [y] ->
+      let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+ 
+ Parameter div : t -> t -> t.
+
+ Parameter spec_div: forall x y, 0 < [y] -> [div x y] = [x] / [y].
+
+ Parameter modulo : t -> t -> t.
+
+ Parameter spec_modulo:
+   forall x y, 0 < [y] -> [modulo x y] = [x] mod [y].
+
+ Parameter gcd : t -> t -> t.
+
+ Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b).
+
+End NType.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
new file mode 100644
index 000000000..115f78be0
--- /dev/null
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -0,0 +1,356 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith.
+Require Import Nnat.
+Require Import NAxioms.
+Require Import NSig.
+
+(** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
+
+Module NSig_NAxioms (N:NType) <: NAxiomsSig.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with N.t.
+Open Local Scope IntScope.
+Notation "[ x ]" := (N.to_Z x) : IntScope.
+Infix "=="  := N.eq (at level 70) : IntScope.
+Notation "0" := N.zero : IntScope.
+Infix "+" := N.add : IntScope.
+Infix "-" := N.sub : IntScope.
+Infix "*" := N.mul : IntScope.
+
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ := N.t.
+Definition NZeq := N.eq.
+Definition NZ0 := N.zero.
+Definition NZsucc := N.succ.
+Definition NZpred := N.pred.
+Definition NZplus := N.add.
+Definition NZminus := N.sub.
+Definition NZtimes := N.mul.
+
+Theorem NZeq_equiv : equiv N.t N.eq.
+Proof.
+repeat split; repeat red; intros; auto; congruence.
+Qed.
+
+Add Relation N.t N.eq
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+ as NZeq_rel.
+
+Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
+Proof.
+unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto.
+Qed.
+
+Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd.
+Proof.
+unfold N.eq; intros.
+generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0).
+destruct N.eq_bool; rewrite N.spec_0; intros.
+rewrite 2 N.spec_pred0; congruence.
+rewrite 2 N.spec_pred; f_equal; auto; try omega.
+Qed.
+
+Add Morphism NZplus with signature N.eq ==> N.eq ==> N.eq as NZplus_wd.
+Proof.
+unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto.
+Qed.
+
+Add Morphism NZminus with signature N.eq ==> N.eq ==> N.eq as NZminus_wd.
+Proof.
+unfold N.eq; intros x x' Hx y y' Hy.
+destruct (Z_lt_le_dec [x] [y]).
+rewrite 2 N.spec_sub0; f_equal; congruence.
+rewrite 2 N.spec_sub; f_equal; congruence.
+Qed.
+
+Add Morphism NZtimes with signature N.eq ==> N.eq ==> N.eq as NZtimes_wd.
+Proof.
+unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto.
+Qed.
+
+Theorem NZpred_succ : forall n, N.pred (N.succ n) == n.
+Proof.
+unfold N.eq; intros.
+rewrite N.spec_pred; rewrite N.spec_succ.
+omega.
+generalize (N.spec_pos n); omega.
+Qed.
+
+Definition N_of_Z z := N.of_N (Zabs_N z).
+
+Section Induction.
+
+Variable A : N.t -> Prop.
+Hypothesis A_wd : predicate_wd N.eq A.
+Hypothesis A0 : A 0.
+Hypothesis AS : forall n, A n <-> A (N.succ n). 
+
+Add Morphism A with signature N.eq ==> iff as A_morph.
+Proof. apply A_wd. Qed.
+
+Let B (z : Z) := A (N_of_Z z).
+
+Lemma B0 : B 0.
+Proof.
+unfold B, N_of_Z; simpl.
+rewrite <- (A_wd 0); auto.
+red; rewrite N.spec_0, N.spec_of_N; auto.
+Qed.
+
+Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1).
+Proof.
+intros z H1 H2.
+unfold B in *. apply -> AS in H2.
+setoid_replace (N_of_Z (z + 1)) with (N.succ (N_of_Z z)); auto.
+unfold N.eq. rewrite N.spec_succ.
+unfold N_of_Z.
+rewrite 2 N.spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith.
+Qed.
+
+Lemma B_holds : forall z : Z, (0 <= z)%Z -> B z.
+Proof.
+exact (natlike_ind B B0 BS).
+Qed.
+
+Theorem NZinduction : forall n, A n.
+Proof.
+intro n. setoid_replace n with (N_of_Z (N.to_Z n)).
+apply B_holds. apply N.spec_pos.
+red; unfold N_of_Z.
+rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+apply N.spec_pos.
+Qed.
+
+End Induction.
+
+Theorem NZplus_0_l : forall n, 0 + n == n.
+Proof.
+intros; red; rewrite N.spec_add, N.spec_0; auto with zarith.
+Qed.
+
+Theorem NZplus_succ_l : forall n m, (N.succ n) + m == N.succ (n + m).
+Proof.
+intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith.
+Qed.
+
+Theorem NZminus_0_r : forall n, n - 0 == n.
+Proof.
+intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith.
+apply N.spec_pos.
+Qed.
+
+Theorem NZminus_succ_r : forall n m, n - (N.succ m) == N.pred (n - m).
+Proof.
+intros; red.
+destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H].
+rewrite N.spec_sub0; auto.
+rewrite N.spec_succ in H.
+rewrite N.spec_pred0; auto.
+destruct (Z_eq_dec [n] [m]).
+rewrite N.spec_sub; auto with zarith.
+rewrite N.spec_sub0; auto with zarith.
+
+rewrite N.spec_sub, N.spec_succ in *; auto.
+rewrite N.spec_pred, N.spec_sub; auto with zarith.
+rewrite N.spec_sub; auto with zarith.
+Qed.
+
+Theorem NZtimes_0_l : forall n, 0 * n == 0.
+Proof.
+intros; red.
+rewrite N.spec_mul, N.spec_0; auto with zarith.
+Qed.
+
+Theorem NZtimes_succ_l : forall n m, (N.succ n) * m == n * m + m.
+Proof.
+intros; red.
+rewrite N.spec_add, 2 N.spec_mul, N.spec_succ; ring.
+Qed.
+
+End NZAxiomsMod.
+
+Definition NZlt := N.lt.
+Definition NZle := N.le.
+Definition NZmin := N.min.
+Definition NZmax := N.max.
+
+Infix "<=" := N.le : IntScope.
+Infix "<" := N.lt : IntScope.
+
+Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z.
+Proof.
+ intros; generalize (N.spec_compare x y).
+ destruct (N.compare x y); auto.
+ intros H; rewrite H; symmetry; apply Zcompare_refl.
+Qed.
+
+Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
+Proof.
+ intros; unfold N.lt, Zlt; rewrite spec_compare_alt; intuition.
+Qed.
+
+Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
+Proof.
+ intros; unfold N.le, Zle; rewrite spec_compare_alt; intuition.
+Qed.
+
+Lemma spec_min : forall x y, [N.min x y] = Zmin [x] [y].
+Proof.
+ intros; unfold N.min, Zmin.
+ rewrite spec_compare_alt; destruct Zcompare; auto.
+Qed.
+
+Lemma spec_max : forall x y, [N.max x y] = Zmax [x] [y].
+Proof.
+ intros; unfold N.max, Zmax.
+ rewrite spec_compare_alt; destruct Zcompare; auto.
+Qed.
+
+Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
+Proof. 
+intros x x' Hx y y' Hy.
+rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.
+Proof.
+intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd.
+Proof.
+intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd.
+Proof.
+intros; red; rewrite 2 spec_min; congruence.
+Qed.
+
+Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd.
+Proof.
+intros; red; rewrite 2 spec_max; congruence.
+Qed.
+
+Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Proof.
+intros.
+unfold N.eq; rewrite spec_lt, spec_le; omega.
+Qed.
+
+Theorem NZlt_irrefl : forall n, ~ n < n.
+Proof.
+intros; rewrite spec_lt; auto with zarith.
+Qed.
+
+Theorem NZlt_succ_r : forall n m, n < (N.succ m) <-> n <= m.
+Proof.
+intros; rewrite spec_lt, spec_le, N.spec_succ; omega.
+Qed.
+
+Theorem NZmin_l : forall n m, n <= m -> N.min n m == n.
+Proof.
+intros n m; unfold N.eq; rewrite spec_le, spec_min.
+generalize (Zmin_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmin_r : forall n m, m <= n -> N.min n m == m.
+Proof.
+intros n m; unfold N.eq; rewrite spec_le, spec_min.
+generalize (Zmin_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmax_l : forall n m, m <= n -> N.max n m == n.
+Proof.
+intros n m; unfold N.eq; rewrite spec_le, spec_max.
+generalize (Zmax_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmax_r : forall n m, n <= m -> N.max n m == m.
+Proof.
+intros n m; unfold N.eq; rewrite spec_le, spec_max.
+generalize (Zmax_spec [n] [m]); omega.
+Qed.
+
+End NZOrdAxiomsMod.
+
+Theorem pred_0 : N.pred 0 == 0.
+Proof.
+red; rewrite N.spec_pred0; rewrite N.spec_0; auto.
+Qed.
+
+Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
+  Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
+Implicit Arguments recursion [A].
+
+Theorem recursion_wd :
+forall (A : Type) (Aeq : relation A),
+  forall a a' : A, Aeq a a' ->
+    forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' ->
+      forall x x' : N.t, x == x' ->
+        Aeq (recursion a f x) (recursion a' f' x').
+Proof.
+unfold fun2_wd, N.eq, fun2_eq.
+intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
+unfold recursion.
+unfold N.to_N.
+rewrite <- Exx'; clear x' Exx'.
+replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])).
+induction (Zabs_nat [x]).
+simpl; auto.
+rewrite N_of_S, 2 Nrect_step; auto.
+destruct [x]; simpl; auto.
+change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
+change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
+Qed.
+
+Theorem recursion_0 :
+  forall (A : Type) (a : A) (f : N.t -> A -> A), recursion a f 0 = a.
+Proof.
+intros A a f; unfold recursion, N.to_N; rewrite N.spec_0; simpl; auto.
+Qed.
+
+Theorem recursion_succ :
+  forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A),
+    Aeq a a -> fun2_wd N.eq Aeq Aeq f ->
+      forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)).
+Proof.
+unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n.
+replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)).
+rewrite Nrect_step.
+apply f_wd; auto.
+unfold N.to_N.
+rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+ apply N.spec_pos.
+
+fold (recursion a f n).
+apply recursion_wd; auto.
+red; auto.
+red; auto.
+unfold N.to_N.
+
+rewrite N.spec_succ.
+change ([n]+1)%Z with (Zsucc [n]).
+apply Z_of_N_eq_rev.
+rewrite Z_of_N_succ.
+rewrite 2 Z_of_N_abs.
+rewrite 2 Zabs_eq; auto.
+generalize (N.spec_pos n); auto with zarith.
+apply N.spec_pos; auto.
+Qed.
+
+End NSig_NAxioms.
diff --git a/theories/Numbers/Rational/BigQ/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v
index 4260c954f..d84efab23 100644
--- a/theories/Numbers/Rational/BigQ/Q0Make.v
+++ b/theories/Numbers/Rational/BigQ/Q0Make.v
@@ -24,6 +24,10 @@ Require Import QMake_base.
 
 Module Q0.
 
+ Import BinInt Zorder.
+ Open Local Scope Q_scope.
+ Open Local Scope Qc_scope.
+
  (** The notation of a rational number is either an integer x,
      interpreted as itself or a pair (x,y) of an integer x and a naturel
      number y interpreted as x/y. The pairs (x,0) and (0,y) are all
diff --git a/theories/Numbers/Rational/BigQ/QbiMake.v b/theories/Numbers/Rational/BigQ/QbiMake.v
index 8ce671a73..e105b36fc 100644
--- a/theories/Numbers/Rational/BigQ/QbiMake.v
+++ b/theories/Numbers/Rational/BigQ/QbiMake.v
@@ -24,6 +24,10 @@ Require Import QMake_base.
 
 Module Qbi.
 
+ Import BinInt Zorder.
+ Open Local Scope Q_scope.
+ Open Local Scope Qc_scope.
+
  (** The notation of a rational number is either an integer x,
      interpreted as itself or a pair (x,y) of an integer x and a naturel
      number y interpreted as x/y. The pairs (x,0) and (0,y) are all
diff --git a/theories/Numbers/Rational/BigQ/QifMake.v b/theories/Numbers/Rational/BigQ/QifMake.v
index 436c13758..1c8caa657 100644
--- a/theories/Numbers/Rational/BigQ/QifMake.v
+++ b/theories/Numbers/Rational/BigQ/QifMake.v
@@ -24,6 +24,10 @@ Require Import QMake_base.
 
 Module Qif.
 
+ Import BinInt.
+ Open Local Scope Q_scope.
+ Open Local Scope Qc_scope.
+
  (** The notation of a rational number is either an integer x,
      interpreted as itself or a pair (x,y) of an integer x and a naturel
      number y interpreted as x/y. The pairs (x,0) and (0,y) are all
diff --git a/theories/Numbers/Rational/BigQ/QpMake.v b/theories/Numbers/Rational/BigQ/QpMake.v
index db6c5926f..b9199357e 100644
--- a/theories/Numbers/Rational/BigQ/QpMake.v
+++ b/theories/Numbers/Rational/BigQ/QpMake.v
@@ -22,6 +22,9 @@ Require Import Qcanon.
 Require Import Qpower.
 Require Import QMake_base.
 
+Notation Nspec_lt := BigNAxiomsMod.NZOrdAxiomsMod.spec_lt.
+Notation Nspec_le := BigNAxiomsMod.NZOrdAxiomsMod.spec_le.
+
 Module Qp.
 
  (** The notation of a rational number is either an integer x,
@@ -186,20 +189,20 @@ Module Qp.
  rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
  rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
  rewrite Zmult_1_r.
- rewrite BigN.succ_pred; auto with zarith.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  rewrite Z2P_correct; auto with zarith.
  rewrite spec_to_N; intros; rewrite Zgcd_div_swap; auto.
  rewrite H; ring.
  intros H3.
  red; simpl.
  rewrite BigZ.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
- rewrite BigN.succ_pred; auto with zarith.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  assert (F: (0 < BigN.to_Z (q / BigN.gcd (BigZ.to_N p) q)%bigN)%Z).
    rewrite BigN.spec_div; auto with zarith.
    rewrite BigN.spec_gcd.
    apply Zgcd_div_pos; auto.
    rewrite BigN.spec_gcd; auto.
- rewrite BigN.succ_pred; auto with zarith.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  rewrite Z2P_correct; auto.
  rewrite Z2P_correct; auto.
  rewrite BigN.spec_div; simpl; rewrite BigN.spec_gcd; auto with zarith.
@@ -315,7 +318,7 @@ Module Qp.
  simpl.
  repeat rewrite BigZ.spec_add.
  repeat rewrite BigZ.spec_mul; simpl.
- rewrite BigN.succ_pred; try apply Qeq_refl; apply spec_succ_pos.
+ rewrite BigN.succ_pred; try apply Qeq_refl; apply lt_0_succ.
  intros p1 n p2.
  match goal with |- [norm ?X ?Y] == _ =>
   apply Qeq_trans with ([Qq X (BigN.pred Y)]);
@@ -325,8 +328,8 @@ Module Qp.
  simpl.
  repeat rewrite BigZ.spec_add.
  repeat rewrite BigZ.spec_mul; simpl.
- rewrite Zplus_comm.
- rewrite BigN.succ_pred; try apply Qeq_refl; apply spec_succ_pos.
+ rewrite BinInt.Zplus_comm.
+ rewrite BigN.succ_pred; try apply Qeq_refl; apply lt_0_succ.
  intros p1 q1 p2 q2.
  match goal with |- [norm ?X ?Y] == _ =>
   apply Qeq_trans with ([Qq X (BigN.pred Y)]);
@@ -391,12 +394,13 @@ Module Qp.
   apply Qeq_refl; auto.
  assert (F1:= spec_succ_pos dx).
  assert (F2:= spec_succ_pos dy).
- rewrite BigN.succ_pred; rewrite BigN.spec_mul.
- rewrite BigZ.spec_mul.
+ rewrite BigN.succ_pred.
+ rewrite BigN.spec_mul; rewrite BigZ.spec_mul.
  assert (tmp: 
   (forall a b, 0 < a -> 0 < b -> Z2P (a * b) = (Z2P a * Z2P b)%positive)%Z).
   intros [|a|a] [|b|b]; simpl; auto; intros; apply False_ind; auto with zarith.
  rewrite tmp; auto; apply Qeq_refl.
+ rewrite Nspec_lt, BigN.spec_0, BigN.spec_mul; auto.
  apply Zmult_lt_0_compat; apply spec_succ_pos.
  Qed.
 
@@ -496,6 +500,7 @@ Module Qp.
  rewrite (Zmult_comm (BigZ.to_Z p1)).
  repeat rewrite Zmult_assoc.
  rewrite Zgcd_div_swap; auto; try ring.
+ rewrite Nspec_lt, BigN.spec_0; auto.
  apply False_ind; generalize F1.
  rewrite (Zdivide_Zdiv_eq
           (Zgcd (BigN.to_Z (BigZ.to_N p2)) (BigN.to_Z (BigN.succ n)))
@@ -556,6 +561,7 @@ Module Qp.
  rewrite (Zmult_comm (BigZ.to_Z p2)).
  repeat rewrite Zmult_assoc.
  rewrite Zgcd_div_swap; auto; try ring.
+ rewrite Nspec_lt, BigN.spec_0; auto.
  apply False_ind; generalize F1.
  rewrite (Zdivide_Zdiv_eq
           (Zgcd (BigN.to_Z (BigZ.to_N p1)) (BigN.to_Z (BigN.succ n)))
@@ -609,7 +615,7 @@ Module Qp.
  assert (F: (0 < BigN.to_Z x)%Z).
    case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith.
  unfold to_Q; rewrite BigZ.spec_1.
- rewrite BigN.succ_pred; auto.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  red; unfold Qinv; simpl.
  generalize F; case BigN.to_Z; auto with zarith.
  intros p Hp; discriminate Hp.
@@ -621,7 +627,7 @@ Module Qp.
  assert (F: (0 < BigN.to_Z x)%Z).
    case (Zle_lt_or_eq _ _ (BigN.spec_pos x)); auto with zarith.
  red; unfold Qinv; simpl.
- rewrite BigN.succ_pred; auto.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  generalize F; case BigN.to_Z; simpl; auto with zarith.
  intros p Hp; discriminate Hp.
  match goal with  |- context[BigN.eq_bool ?X ?Y] => 
@@ -632,7 +638,7 @@ Module Qp.
  assert (F: (0 < BigN.to_Z nx)%Z).
    case (Zle_lt_or_eq _ _ (BigN.spec_pos nx)); auto with zarith.
  red; unfold Qinv; simpl.
- rewrite BigN.succ_pred; auto.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  rewrite BigN.spec_succ; rewrite Z2P_correct; auto with zarith.
  generalize F; case BigN.to_Z; auto with zarith.
  intros p Hp; discriminate Hp.
@@ -645,12 +651,12 @@ Module Qp.
  assert (F: (0 < BigN.to_Z nx)%Z).
    case (Zle_lt_or_eq _ _ (BigN.spec_pos nx)); auto with zarith.
  red; unfold Qinv; simpl.
- rewrite BigN.succ_pred; auto.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  rewrite BigN.spec_succ; rewrite Z2P_correct; auto with zarith.
  generalize F; case BigN.to_Z; auto with zarith.
- simpl; intros. 
+ simpl; intros.
  match goal with  |- (?X = Zneg ?Y)%Z => 
-   replace (Zneg Y) with (Zopp (Zpos Y));
+   replace (Zneg Y) with (-(Zpos Y))%Z;
    try rewrite Z2P_correct; auto with zarith
  end.
  rewrite Zpos_mult_morphism; 
@@ -704,7 +710,7 @@ Definition inv_norm x :=
    generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
  end; rewrite BigN.spec_1; intros H1.
  red; simpl.
- rewrite BigN.succ_pred; auto.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  rewrite Z2P_correct; try rewrite H1; auto with zarith.
   apply Qeq_refl.
  match goal with  |- context[BigN.eq_bool ?X ?Y] => 
@@ -717,7 +723,7 @@ Definition inv_norm x :=
    generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
  end; rewrite BigN.spec_1; intros H1.
  red; simpl.
- rewrite BigN.succ_pred; auto.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  rewrite Z2P_correct; try rewrite H1; auto with zarith.
   apply Qeq_refl.
  case nx; clear nx; intros nx.
@@ -730,6 +736,7 @@ Definition inv_norm x :=
  end; rewrite BigN.spec_1; intros H1.
  red; simpl.
  rewrite BigN.succ_pred; try rewrite H1; auto with zarith.
+ rewrite Nspec_lt, BigN.spec_0, H1; auto with zarith.
  apply Qeq_refl.
  match goal with  |- context[BigN.eq_bool ?X ?Y] => 
    generalize (BigN.spec_eq_bool X Y); case BigN.eq_bool
@@ -740,6 +747,7 @@ Definition inv_norm x :=
  end; rewrite BigN.spec_1; intros H1.
  red; simpl.
  rewrite BigN.succ_pred; try rewrite H1; auto with zarith.
+ rewrite Nspec_lt, BigN.spec_0, H1; auto with zarith.
  apply Qeq_refl.
  Qed.
 
@@ -791,7 +799,7 @@ Definition inv_norm x :=
  assert (F1 : (0 < BigN.to_Z (BigN.square (BigN.succ dx)))%Z).
    rewrite BigN.spec_square; apply Zmult_lt_0_compat;
      auto with zarith.
- rewrite BigN.succ_pred; auto.
+ rewrite BigN.succ_pred by (rewrite Nspec_lt, BigN.spec_0; auto).
  rewrite Zpos_mult_morphism.
  repeat rewrite Z2P_correct; auto with zarith.
  repeat rewrite BigN.spec_succ; auto with zarith.
@@ -837,7 +845,7 @@ Definition inv_norm x :=
  assert (F2: (0 < BigN.to_Z (BigN.succ dx) ^ ' p)%Z).
   unfold Zpower; apply Zpower_pos_pos; auto.
  unfold power_pos; red; simpl.
- rewrite BigN.succ_pred; rewrite BigN.spec_power_pos; auto.
+ rewrite BigN.succ_pred, BigN.spec_power_pos.
  rewrite Z2P_correct; auto.
  generalize (Qpower_decomp p (BigZ.to_Z nx) 
                (Z2P (BigN.to_Z (BigN.succ dx)))).
@@ -846,6 +854,7 @@ Definition inv_norm x :=
  unfold Qeq; simpl; intros HH.
  rewrite HH.
  rewrite BigZ.spec_power_pos; simpl; ring.
+ rewrite Nspec_lt, BigN.spec_0, BigN.spec_power_pos; auto.
  Qed.
 
  Theorem spec_power_posc x p: [[power_pos x p]] = [[x]] ^ nat_of_P p.
diff --git a/theories/Numbers/Rational/BigQ/QvMake.v b/theories/Numbers/Rational/BigQ/QvMake.v
index 59da4da6d..3f51e7063 100644
--- a/theories/Numbers/Rational/BigQ/QvMake.v
+++ b/theories/Numbers/Rational/BigQ/QvMake.v
@@ -24,6 +24,10 @@ Require Import QMake_base.
 
 Module Qv.
 
+ Import BinInt Zorder.
+ Open Local Scope Q_scope.
+ Open Local Scope Qc_scope.
+
  (** The notation of a rational number is either an integer x,
      interpreted as itself or a pair (x,y) of an integer x and a naturel
      number y interpreted as x/y. All functions maintain the invariant