Numbers: new functions pow, even, odd + many reorganisations

 - Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct
 - The axiomatisations of the different fonctions are now in {N,Z}Axioms.v
   apart for Z division (three separate flavours in there own files).
   Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig.
 - In NAxioms, the recursion field isn't that useful, since we axiomatize
   other functions and not define them (apart in the toy NDefOps.v).
   We leave recursion there, but in a separate NAxiomsFullSig.
 - On Z, the pow function is specified to behave as Zpower : a^(-1)=0
 - In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t
   These pow could be more clever (we convert 2nd arg to N and use pow_N).
   Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly
 - In BigN, is_even is now even, its spec is changed to use Zeven_bool.
   We add an odd. In BigZ, we add even and odd.
 - In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow
   to implement pow. This Zpow should replace the current linear Zpower
   someday.
 - In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions,
   and we modify the div and mod functions for them to be linear, structural,
   tail-recursive.

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

21 files changed, 682 insertions, 117 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index aff298117..2c386a980 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -10,8 +10,8 @@
 
 Require Export ZBase.
 
-Module ZAddPropFunct (Import Z : ZAxiomsSig').
-Include ZBasePropFunct Z.
+Module ZAddProp (Import Z : ZAxiomsMiniSig').
+Include ZBaseProp Z.
 
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
@@ -287,5 +287,5 @@ Qed.
 
 (** Of course, there are many other variants *)
 
-End ZAddPropFunct.
+End ZAddProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index bdc4d21e9..eb27e6378 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -10,8 +10,8 @@
 
 Require Export ZLt.
 
-Module ZAddOrderPropFunct (Import Z : ZAxiomsSig').
-Include ZOrderPropFunct Z.
+Module ZAddOrderProp (Import Z : ZAxiomsMiniSig').
+Include ZOrderProp Z.
 
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
@@ -293,6 +293,6 @@ End PosNeg.
 
 Ltac zero_pos_neg n := induction_maker n ltac:(apply zero_pos_neg).
 
-End ZAddOrderPropFunct.
+End ZAddOrderProp.
 
 
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index c0d3db92b..38855a85d 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -9,8 +9,18 @@
 (************************************************************************)
 
 Require Export NZAxioms.
+Require Import NZPow.
 
-Set Implicit Arguments.
+(** We obtain integers by postulating that successor of predecessor
+    is identity. *)
+
+Module Type ZAxiom (Import Z : NZAxiomsSig').
+ Axiom succ_pred : forall n, S (P n) == n.
+End ZAxiom.
+
+(** For historical reasons, ZAxiomsMiniSig isn't just NZ + ZAxiom,
+    we also add an [opp] function, that can be seen as a shortcut
+    for [sub 0]. *)
 
 Module Type Opp (Import T:Typ).
  Parameter Inline opp : t -> t.
@@ -22,15 +32,59 @@ End OppNotation.
 
 Module Type Opp' (T:Typ) := Opp T <+ OppNotation T.
 
-(** We obtain integers by postulating that every number has a predecessor. *)
-
 Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z).
  Declare Instance opp_wd : Proper (eq==>eq) opp.
- Axiom succ_pred : forall n, S (P n) == n.
  Axiom opp_0 : - 0 == 0.
  Axiom opp_succ : forall n, - (S n) == P (- n).
 End IsOpp.
 
-Module Type ZAxiomsSig := NZOrdAxiomsSig <+ Opp <+ IsOpp.
-Module Type ZAxiomsSig' := NZOrdAxiomsSig' <+ Opp' <+ IsOpp.
+Module Type ZAxiomsMiniSig := NZOrdAxiomsSig <+ ZAxiom <+ Opp <+ IsOpp.
+Module Type ZAxiomsMiniSig' := NZOrdAxiomsSig' <+ ZAxiom <+ Opp' <+ IsOpp.
+
+(** Other functions and their specifications *)
+
+(** Absolute value *)
+
+Module Type HasAbs(Import Z : ZAxiomsMiniSig').
+ Parameter Inline abs : t -> t.
+ Axiom abs_eq : forall n, 0<=n -> abs n == n.
+ Axiom abs_neq : forall n, n<=0 -> abs n == -n.
+End HasAbs.
+
+(** A sign function *)
+
+Module Type HasSgn (Import Z : ZAxiomsMiniSig').
+ Parameter Inline sgn : t -> t.
+ Axiom sgn_null : forall n, n==0 -> sgn n == 0.
+ Axiom sgn_pos : forall n, 0<n -> sgn n == 1.
+ Axiom sgn_neg : forall n, n<0 -> sgn n == -(1).
+End HasSgn.
+
+(** Parity functions *)
+
+Module Type Parity (Import Z : ZAxiomsMiniSig').
+ Parameter Inline even odd : t -> bool.
+ Definition Even n := exists m, n == 2*m.
+ Definition Odd n := exists m, n == 2*m+1.
+ Axiom even_spec : forall n, even n = true <-> Even n.
+ Axiom odd_spec : forall n, odd n = true <-> Odd n.
+End Parity.
+
+(** For the power function, we just add to NZPow an addition spec *)
+
+Module Type ZPowSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Pow' Z).
+ Axiom pow_neg : forall a b, b<0 -> a^b == 0.
+End ZPowSpecNeg.
+
+
+(** Let's group everything *)
+
+Module Type ZAxiomsSig :=
+  ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
+   <+ NZPow.NZPow <+ ZPowSpecNeg.
+Module Type ZAxiomsSig' :=
+  ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
+   <+ NZPow.NZPow' <+ ZPowSpecNeg.
+
 
+(** Division is left apart, since many different flavours are available *)
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 1c9844322..f9bd8dba3 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -12,8 +12,8 @@ Require Export Decidable.
 Require Export ZAxioms.
 Require Import NZProperties.
 
-Module ZBasePropFunct (Import Z : ZAxiomsSig').
-Include NZPropFunct Z.
+Module ZBaseProp (Import Z : ZAxiomsMiniSig').
+Include NZProp Z.
 
 (* Theorems that are true for integers but not for natural numbers *)
 
@@ -27,5 +27,5 @@ Proof.
 intros n1 n2; split; [apply pred_inj | apply pred_wd].
 Qed.
 
-End ZBasePropFunct.
+End ZBaseProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 076815b2e..bb5c2410f 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -23,17 +23,17 @@
 
 Require Import ZAxioms ZProperties NZDiv.
 
-Module Type ZDivSpecific (Import Z : ZAxiomsExtSig')(Import DM : DivMod' Z).
+Module Type ZDivSpecific (Import Z : ZAxiomsSig')(Import DM : DivMod' Z).
  Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b.
 End ZDivSpecific.
 
-Module Type ZDiv (Z:ZAxiomsExtSig)
+Module Type ZDiv (Z:ZAxiomsSig)
  := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
 
-Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv.
-Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation.
+Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
 
-Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
+Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -49,7 +49,7 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
   apply mod_always_pos.
   Qed.
  End ZD.
- Module Import NZDivP := NZDivPropFunct Z ZP ZD.
+ Module Import NZDivP := NZDivProp Z ZP ZD.
 
 (** Another formulation of the main equation *)
 
@@ -601,5 +601,5 @@ now apply mod_mul.
 Qed.
 
 
-End ZDivPropFunct.
+End ZDivProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index fd052c2ef..c619d8b07 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -34,10 +34,10 @@ End ZDivSpecific.
 Module Type ZDiv (Z:ZAxiomsSig)
  := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
 
-Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv.
-Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation.
+Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
 
-Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
+Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -50,7 +50,7 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof. intros. now apply mod_pos_bound. Qed.
  End ZD.
- Module Import NZDivP := NZDivPropFunct Z ZP ZD.
+ Module Import NZDivP := NZDivProp Z ZP ZD.
 
 (** Another formulation of the main equation *)
 
@@ -628,5 +628,5 @@ rewrite Hc, mul_comm.
 now apply mod_mul.
 Qed.
 
-End ZDivPropFunct.
+End ZDivProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 4411b8dca..027223415 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -35,14 +35,14 @@ End ZDivSpecific.
 Module Type ZDiv (Z:ZAxiomsSig)
  := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
 
-Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv.
-Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation.
+Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
 
-Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
+Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Import NZDivP := NZDivPropFunct Z ZP Z.
+ Module Import NZDivP := NZDivProp Z ZP Z.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
@@ -528,5 +528,5 @@ Proof.
  intros (c,Hc). rewrite Hc, mul_comm. now apply mod_mul.
 Qed.
 
-End ZDivPropFunct.
+End ZDivProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index ed812fcc3..540e17cb4 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -10,8 +10,8 @@
 
 Require Export ZMul.
 
-Module ZOrderPropFunct (Import Z : ZAxiomsSig').
-Include ZMulPropFunct Z.
+Module ZOrderProp (Import Z : ZAxiomsMiniSig').
+Include ZMulProp Z.
 
 (** Instances of earlier theorems for m == 0 *)
 
@@ -128,5 +128,5 @@ setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m.
 apply <- eq_opp_r. now rewrite opp_pred, opp_0.
 Qed.
 
-End ZOrderPropFunct.
+End ZOrderProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v
index 53709a906..4e653fee4 100644
--- a/theories/Numbers/Integer/Abstract/ZMaxMin.v
+++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v
@@ -10,8 +10,8 @@ Require Import ZAxioms ZMulOrder GenericMinMax.
 
 (** * Properties of minimum and maximum specific to integer numbers *)
 
-Module Type ZMaxMinProp (Import Z : ZAxiomsSig').
-Include ZMulOrderPropFunct Z.
+Module Type ZMaxMinProp (Import Z : ZAxiomsMiniSig').
+Include ZMulOrderProp Z.
 
 (** The following results are concrete instances of [max_monotone]
     and similar lemmas. *)
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 05a285f21..68eca3305 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -10,8 +10,8 @@
 
 Require Export ZAdd.
 
-Module ZMulPropFunct (Import Z : ZAxiomsSig').
-Include ZAddPropFunct Z.
+Module ZMulProp (Import Z : ZAxiomsMiniSig').
+Include ZAddProp Z.
 
 (** A note on naming: right (correspondingly, left) distributivity
     happens when the sum is multiplied by a number on the right
@@ -65,6 +65,6 @@ intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p);
 now apply mul_sub_distr_l.
 Qed.
 
-End ZMulPropFunct.
+End ZMulProp.
 
 
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 4682ad8b6..76428584d 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -10,8 +10,8 @@
 
 Require Export ZAddOrder.
 
-Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig').
-Include ZAddOrderPropFunct Z.
+Module Type ZMulOrderProp (Import Z : ZAxiomsMiniSig').
+Include ZAddOrderProp Z.
 
 Local Notation "- 1" := (-(1)).
 
@@ -227,5 +227,5 @@ apply mul_lt_mono_nonneg.
 now apply lt_le_incl. assumption. apply le_0_1. assumption.
 Qed.
 
-End ZMulOrderPropFunct.
+End ZMulOrderProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
new file mode 100644
index 000000000..1ababfe5c
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -0,0 +1,196 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Bool ZMulOrder.
+
+(** Properties of [even] and [odd]. *)
+
+(** NB: most parts of [NParity] and [ZParity] are common,
+    but it is difficult to share them in NZ, since
+    initial proofs [Even_or_Odd] and [Even_Odd_False] must
+    be proved differently *)
+
+Module Type ZParityProp (Import Z : ZAxiomsSig')
+                        (Import ZP : ZMulOrderProp Z).
+
+Instance Even_wd : Proper (eq==>iff) Even.
+Proof. unfold Even. solve_predicate_wd. Qed.
+
+Instance Odd_wd : Proper (eq==>iff) Odd.
+Proof. unfold Odd. solve_predicate_wd. Qed.
+
+Instance even_wd : Proper (eq==>Logic.eq) even.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd.
+Qed.
+
+Instance odd_wd : Proper (eq==>Logic.eq) odd.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd.
+Qed.
+
+Lemma Even_or_Odd : forall x, Even x \/ Odd x.
+Proof.
+ nzinduct x.
+ left. exists 0. now nzsimpl.
+ intros x.
+ split; intros [(y,H)|(y,H)].
+ right. exists y. rewrite H. now nzsimpl.
+ left. exists (S y). rewrite H. now nzsimpl.
+ right. exists (P y). rewrite <- succ_inj_wd. rewrite H.
+  nzsimpl. now rewrite <- add_succ_l, <- add_succ_r, succ_pred.
+ left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl.
+Qed.
+
+Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
+Proof.
+ intros. nzsimpl. apply lt_succ_r. now apply add_le_mono.
+Qed.
+
+Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
+Proof.
+ intros. nzsimpl.
+ rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
+ apply add_le_mono; now apply le_succ_l.
+Qed.
+
+Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.
+Proof.
+intros x (y,E) (z,O). rewrite O in E; clear O.
+destruct (le_gt_cases y z) as [LE|GT].
+generalize (double_below _ _ LE); order.
+generalize (double_above _ _ GT); order.
+Qed.
+
+Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
+Proof.
+ intros.
+ destruct (Even_or_Odd n) as [H|H].
+ rewrite <- even_spec in H. now rewrite H.
+ rewrite <- odd_spec in H. now rewrite H, orb_true_r.
+Qed.
+
+Lemma negb_odd_even : forall n, negb (odd n) = even n.
+Proof.
+ intros.
+ generalize (Even_or_Odd n) (Even_Odd_False n).
+ rewrite <- even_spec, <- odd_spec.
+ destruct (odd n), (even n); simpl; intuition.
+Qed.
+
+Lemma negb_even_odd : forall n, negb (even n) = odd n.
+Proof.
+ intros. rewrite <- negb_odd_even. apply negb_involutive.
+Qed.
+
+Lemma even_0 : even 0 = true.
+Proof.
+ rewrite even_spec. exists 0. now nzsimpl.
+Qed.
+
+Lemma odd_1 : odd 1 = true.
+Proof.
+ rewrite odd_spec. exists 0. now nzsimpl.
+Qed.
+
+Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
+Proof.
+ split; intros (m,H).
+ exists m. apply succ_inj. now rewrite add_1_r in H.
+ exists m. rewrite add_1_r. now apply succ_wd.
+Qed.
+
+Lemma odd_succ_even : forall n, odd (S n) = even n.
+Proof.
+ intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec.
+ apply Odd_succ_Even.
+Qed.
+
+Lemma even_succ_odd : forall n, even (S n) = odd n.
+Proof.
+ intros. now rewrite <- negb_odd_even, odd_succ_even, negb_even_odd.
+Qed.
+
+Lemma Even_succ_Odd : forall n, Even (S n) <-> Odd n.
+Proof.
+ intros. now rewrite <- even_spec, even_succ_odd, odd_spec.
+Qed.
+
+Lemma odd_pred_even : forall n, odd (P n) = even n.
+Proof.
+ intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ_odd.
+Qed.
+
+Lemma even_pred_odd : forall n, even (P n) = odd n.
+Proof.
+ intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ_even.
+Qed.
+
+Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m).
+Proof.
+ intros.
+ case_eq (even n); case_eq (even m);
+  rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec;
+  intros (m',Hm) (n',Hn).
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
+ exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1.
+Qed.
+
+Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
+Proof.
+ intros. rewrite <- !negb_even_odd. rewrite even_add.
+ now destruct (even n), (even m).
+Qed.
+
+Lemma even_mul : forall n m, even (mul n m) = even n || even m.
+Proof.
+ intros.
+ case_eq (even n); simpl; rewrite ?even_spec.
+ intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
+ case_eq (even m); simpl; rewrite ?even_spec.
+ intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2).
+ (* odd / odd *)
+ rewrite <- !negb_true_iff, !negb_even_odd, !odd_spec.
+ intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m').
+ rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r.
+ now rewrite add_shuffle1, add_assoc, !mul_assoc.
+Qed.
+
+Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.
+Proof.
+ intros. rewrite <- !negb_even_odd. rewrite even_mul.
+ now destruct (even n), (even m).
+Qed.
+
+Lemma even_opp : forall n, even (-n) = even n.
+Proof.
+ assert (H : forall n, Even n -> Even (-n)).
+  intros n (m,H). exists (-m). rewrite mul_opp_r. now apply opp_wd.
+ intros. rewrite eq_iff_eq_true, !even_spec.
+ split. rewrite <- (opp_involutive n) at 2. apply H.
+ apply H.
+Qed.
+
+Lemma odd_opp : forall n, odd (-n) = odd n.
+Proof.
+ intros. rewrite <- !negb_even_odd. now rewrite even_opp.
+Qed.
+
+Lemma even_sub : forall n m, even (n-m) = Bool.eqb (even n) (even m).
+Proof.
+ intros. now rewrite <- add_opp_r, even_add, even_opp.
+Qed.
+
+Lemma odd_sub : forall n m, odd (n-m) = xorb (odd n) (odd m).
+Proof.
+ intros. now rewrite <- add_opp_r, odd_add, odd_opp.
+Qed.
+
+End ZParityProp.
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
new file mode 100644
index 000000000..9de681375
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -0,0 +1,151 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Properties of the power function *)
+
+Require Import Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow.
+
+Module ZPowProp (Import Z : ZAxiomsSig')(Import ZM : ZMulOrderProp Z)
+ (Import ZP : ZParityProp Z ZM)(Import ZS : ZSgnAbsProp Z ZM).
+ Include NZPowProp Z ZM Z.
+
+(** Many results are directly the same as in NZPow, hence
+    the Include above. We extend nonetheless a few of them,
+    and add some results concerning negative first arg.
+*)
+
+Lemma pow_mul_l' : forall a b c, (a*b)^c == a^c * b^c.
+Proof.
+ intros a b c. destruct (le_gt_cases 0 c). now apply pow_mul_l.
+ rewrite !pow_neg by trivial. now nzsimpl.
+Qed.
+
+Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b.
+Proof.
+ intros a b Ha. destruct (le_gt_cases 0 b).
+ now apply pow_nonneg_nonneg.
+ rewrite !pow_neg by trivial. order.
+Qed.
+
+Lemma pow_le_mono_l' : forall a b c, 0<=a<=b -> a^c <= b^c.
+Proof.
+ intros a b c. destruct (le_gt_cases 0 c). now apply pow_le_mono_l.
+ rewrite !pow_neg by trivial. order.
+Qed.
+
+(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *)
+
+Lemma pow_le_mono_r' : forall a b c, 0<a -> b<=c -> a^b <= a^c.
+Proof.
+ intros a b c. destruct (le_gt_cases 0 b).
+ intros. apply pow_le_mono_r; try split; trivial.
+ rewrite !pow_neg by trivial.
+ intros. apply pow_nonneg. order.
+Qed.
+
+Lemma pow_le_mono' : forall a b c d, 0<a<=c -> b<=d ->
+ a^b <= c^d.
+Proof.
+ intros a b c d. destruct (le_gt_cases 0 b).
+ intros. apply pow_le_mono. trivial. split; trivial.
+ rewrite !pow_neg by trivial.
+ intros. apply pow_nonneg. intuition order.
+Qed.
+
+(** Parity of power *)
+
+Lemma even_pow : forall a b, 0<b -> even (a^b) = even a.
+Proof.
+ intros a b Hb. apply lt_ind with (4:=Hb). solve_predicate_wd.
+ now nzsimpl.
+ clear b Hb. intros b Hb IH. nzsimpl; [|order].
+ rewrite even_mul, IH. now destruct (even a).
+Qed.
+
+Lemma odd_pow : forall a b, 0<b -> odd (a^b) = odd a.
+Proof.
+ intros. now rewrite <- !negb_even_odd, even_pow.
+Qed.
+
+(** Properties of power of negative numbers *)
+
+Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b.
+Proof.
+ intros a b (c,H). rewrite H.
+ destruct (le_gt_cases 0 c).
+ assert (0 <= 2) by (apply le_le_succ_r, le_0_1).
+ rewrite 2 pow_mul_r; trivial.
+ rewrite 2 pow_2_r.
+ now rewrite mul_opp_opp.
+ assert (2*c < 0).
+  apply mul_pos_neg; trivial. rewrite lt_succ_r. apply le_0_1.
+ now rewrite !pow_neg.
+Qed.
+
+Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
+Proof.
+ intros a b (c,H). rewrite H.
+ destruct (le_gt_cases 0 c) as [LE|GT].
+ assert (0 <= 2*c).
+  apply mul_nonneg_nonneg; trivial.
+  apply le_le_succ_r, le_0_1.
+ rewrite add_succ_r, add_0_r, !pow_succ_r; trivial.
+ rewrite pow_opp_even by (now exists c).
+ apply mul_opp_l.
+ apply double_above in GT. rewrite mul_0_r in GT.
+ rewrite !pow_neg by trivial. now rewrite opp_0.
+Qed.
+
+Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b.
+Proof.
+ intros. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ.
+ reflexivity.
+ symmetry. now apply pow_opp_even.
+Qed.
+
+Lemma pow_even_nonneg : forall a b, Even b -> 0 <= a^b.
+Proof.
+ intros. rewrite pow_even_abs by trivial.
+ apply pow_nonneg, abs_nonneg.
+Qed.
+
+Lemma pow_odd_abs_sgn : forall a b, Odd b -> a^b == sgn a * (abs a)^b.
+Proof.
+ intros a b H.
+ destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.
+ nzsimpl.
+ rewrite abs_eq; order.
+ rewrite <- EQ'. nzsimpl.
+ destruct (le_gt_cases 0 b).
+ apply pow_0_l.
+ assert (b~=0) by
+  (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0).
+ order.
+ now rewrite pow_neg.
+ rewrite abs_neq by order.
+ rewrite pow_opp_odd; trivial.
+ now rewrite mul_opp_opp, mul_1_l.
+Qed.
+
+Lemma pow_odd_sgn : forall a b, 0<=b -> Odd b -> sgn (a^b) == sgn a.
+Proof.
+ intros a b Hb H.
+ destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.
+ apply sgn_pos. apply pow_pos_nonneg; trivial.
+ rewrite <- EQ'. rewrite pow_0_l. apply sgn_0.
+ assert (b~=0) by
+  (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0).
+ order.
+ apply sgn_neg.
+ rewrite <- (opp_involutive a). rewrite pow_opp_odd by trivial.
+ apply opp_neg_pos.
+ apply pow_pos_nonneg; trivial.
+ now apply opp_pos_neg.
+Qed.
+
+End ZPowProp.
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 5463bf2b1..7b9c6f452 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -6,17 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export ZAxioms ZMaxMin ZSgnAbs.
+Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow.
 
-(** This functor summarizes all known facts about Z.
-    For the moment it is only an alias to the last functor which
-    subsumes all others, plus properties of [sgn] and [abs].
-*)
+(** This functor summarizes all known facts about Z. *)
 
-Module Type ZPropSig (Z:ZAxiomsExtSig) :=
- ZMaxMinProp Z <+ ZSgnAbsPropSig Z.
+Module Type ZProp (Z:ZAxiomsSig) :=
+ ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z.
 
-Module ZPropFunct (Z:ZAxiomsExtSig) <: ZPropSig Z.
- Include ZPropSig Z.
-End ZPropFunct.
 
diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
index 540749632..6d90bc0fd 100644
--- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v
+++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
@@ -6,20 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export ZMulOrder.
+(** Properties of [abs] and [sgn] *)
 
-(** An axiomatization of [abs]. *)
-
-Module Type HasAbs(Import Z : ZAxiomsSig').
- Parameter Inline abs : t -> t.
- Axiom abs_eq : forall n, 0<=n -> abs n == n.
- Axiom abs_neq : forall n, n<=0 -> abs n == -n.
-End HasAbs.
+Require Import ZMulOrder.
 
 (** Since we already have [max], we could have defined [abs]. *)
 
-Module GenericAbs (Import Z : ZAxiomsSig')
-                  (Import ZP : ZMulOrderPropFunct Z) <: HasAbs Z.
+Module GenericAbs (Import Z : ZAxiomsMiniSig')
+                  (Import ZP : ZMulOrderProp Z) <: HasAbs Z.
  Definition abs n := max n (-n).
  Lemma abs_eq : forall n, 0<=n -> abs n == n.
  Proof.
@@ -35,22 +29,13 @@ Module GenericAbs (Import Z : ZAxiomsSig')
  Qed.
 End GenericAbs.
 
-(** An Axiomatization of [sgn]. *)
-
-Module Type HasSgn (Import Z : ZAxiomsSig').
- Parameter Inline sgn : t -> t.
- Axiom sgn_null : forall n, n==0 -> sgn n == 0.
- Axiom sgn_pos : forall n, 0<n -> sgn n == 1.
- Axiom sgn_neg : forall n, n<0 -> sgn n == -(1).
-End HasSgn.
-
 (** We can deduce a [sgn] function from a [compare] function *)
 
-Module Type ZDecAxiomsSig := ZAxiomsSig <+ HasCompare.
-Module Type ZDecAxiomsSig' := ZAxiomsSig' <+ HasCompare.
+Module Type ZDecAxiomsSig := ZAxiomsMiniSig <+ HasCompare.
+Module Type ZDecAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare.
 
 Module Type GenericSgn (Import Z : ZDecAxiomsSig')
-                       (Import ZP : ZMulOrderPropFunct Z) <: HasSgn Z.
+                       (Import ZP : ZMulOrderProp Z) <: HasSgn Z.
  Definition sgn n :=
   match compare 0 n with Eq => 0 | Lt => 1 | Gt => -(1) end.
  Lemma sgn_null : forall n, n==0 -> sgn n == 0.
@@ -61,11 +46,11 @@ Module Type GenericSgn (Import Z : ZDecAxiomsSig')
  Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
 End GenericSgn.
 
-Module Type ZAxiomsExtSig := ZAxiomsSig <+ HasAbs <+ HasSgn.
-Module Type ZAxiomsExtSig' := ZAxiomsSig' <+ HasAbs <+ HasSgn.
 
-Module Type ZSgnAbsPropSig (Import Z : ZAxiomsExtSig')
-                           (Import ZP : ZMulOrderPropFunct Z).
+(** Derived properties of [abs] and [sgn] *)
+
+Module Type ZSgnAbsProp (Import Z : ZAxiomsSig')
+                        (Import ZP : ZMulOrderProp Z).
 
 Ltac destruct_max n :=
  destruct (le_ge_cases 0 n);
@@ -343,6 +328,15 @@ Proof.
  rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl.
 Qed.
 
-End ZSgnAbsPropSig.
+Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x.
+Proof.
+ intros.
+ destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.
+ apply sgn_pos, lt_0_1.
+ now apply sgn_null.
+ apply sgn_neg. rewrite opp_neg_pos. apply lt_0_1.
+Qed.
+
+End ZSgnAbsProp.
 
 
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 64553161f..6c9dc77c1 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -29,7 +29,7 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
  ZMake.Make BigN <+ ZTypeIsZAxioms
- <+ !ZPropSig <+ !ZDivPropFunct <+ HasEqBool2Dec
+ <+ !ZProp <+ !ZDivProp <+ HasEqBool2Dec
  <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
 
 (** Notations about [BigZ] *)
@@ -60,8 +60,9 @@ Arguments Scope BigZ.compare [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.min [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.max [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.power_pos [bigZ_scope positive_scope].
-Arguments Scope BigZ.power [bigZ_scope N_scope].
+Arguments Scope BigZ.pow_pos [bigZ_scope positive_scope].
+Arguments Scope BigZ.pow_N [bigZ_scope N_scope].
+Arguments Scope BigZ.pow [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.sqrt [bigZ_scope].
 Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
@@ -74,7 +75,7 @@ Infix "-" := BigZ.sub : bigZ_scope.
 Notation "- x" := (BigZ.opp x) : bigZ_scope.
 Infix "*" := BigZ.mul : bigZ_scope.
 Infix "/" := BigZ.div : bigZ_scope.
-Infix "^" := BigZ.power : bigZ_scope.
+Infix "^" := BigZ.pow : bigZ_scope.
 Infix "?=" := BigZ.compare : bigZ_scope.
 Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
 Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope.
@@ -136,11 +137,13 @@ Qed.
 Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y.
 Proof. now apply BigZ.eqb_eq. Qed.
 
-Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq (@id N) BigZ.power.
+Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n).
+
+Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow.
 Proof.
 constructor.
-intros. red. rewrite BigZ.spec_power. unfold id.
-destruct Zpower_theory as [EQ]. rewrite EQ.
+intros. unfold BigZ.eq, BigZ_of_N. rewrite BigZ.spec_pow, BigZ.spec_of_Z.
+rewrite Zpower_theory.(rpow_pow_N).
 destruct n; simpl. reflexivity.
 induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto.
 Qed.
@@ -178,16 +181,25 @@ Ltac BigZcst t :=
  | false => constr:NotConstant
  end.
 
+Ltac BigZ_to_N t :=
+ match t with
+ | BigZ.Pos ?t => BigN_to_N t
+ | BigZ.zero => constr:0%N
+ | BigZ.one => constr:1%N
+ | _ => constr:NotConstant
+ end.
+
 (** Registration for the "ring" tactic *)
 
 Add Ring BigZr : BigZring
  (decidable BigZeqb_correct,
   constants [BigZcst],
-  power_tac BigZpower [Ncst],
+  power_tac BigZpower [BigZ_to_N],
   div BigZdiv).
 
 Section TestRing.
-Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
+Local Notation "2" := (BigZ.Pos (BigN.N0 2%int31)) : bigZ_scope.
+Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x.
 Proof.
 intros. ring_simplify. reflexivity.
 Qed.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 6d14337ab..fb760bdf5 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -271,23 +271,23 @@ Module Make (N:NType) <: ZType.
  unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring.
  Qed.
 
- Definition power_pos x p :=
+ Definition pow_pos x p :=
   match x with
-  | Pos nx => Pos (N.power_pos nx p)
+  | Pos nx => Pos (N.pow_pos nx p)
   | Neg nx =>
     match p with
     | xH => x
-    | xO _ => Pos (N.power_pos nx p)
-    | xI _ => Neg (N.power_pos nx p)
+    | xO _ => Pos (N.pow_pos nx p)
+    | xI _ => Neg (N.pow_pos nx p)
     end
   end.
 
- Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
+ Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n.
  Proof.
  assert (F0: forall x, (-x)^2 = x^2).
    intros x; rewrite Zpower_2; ring.
- unfold power_pos, to_Z; intros [x | x] [p | p |];
-   try rewrite N.spec_power_pos; try ring.
+ unfold pow_pos, to_Z; intros [x | x] [p | p |];
+   try rewrite N.spec_pow_pos; try ring.
  assert (F: 0 <= 2 * Zpos p).
   assert (0 <= Zpos p); auto with zarith.
  rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith.
@@ -300,18 +300,32 @@ Module Make (N:NType) <: ZType.
  rewrite F0; ring.
  Qed.
 
- Definition power x n :=
+ Definition pow_N x n :=
   match n with
   | N0 => one
-  | Npos p => power_pos x p
+  | Npos p => pow_pos x p
   end.
 
- Theorem spec_power: forall x n, to_Z (power x n) = to_Z x ^ Z_of_N n.
+ Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z_of_N n.
  Proof.
- destruct n; simpl. rewrite N.spec_1; reflexivity.
- apply spec_power_pos.
+ destruct n; simpl. apply N.spec_1.
+ apply spec_pow_pos.
  Qed.
 
+ Definition pow x y :=
+  match to_Z y with
+  | Z0 => one
+  | Zpos p => pow_pos x p
+  | Zneg p => zero
+  end.
+
+ Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y.
+ Proof.
+ intros. unfold pow. destruct (to_Z y); simpl.
+ apply N.spec_1.
+ apply spec_pow_pos.
+ apply N.spec_0.
+ Qed.
 
  Definition sqrt x :=
   match x with
@@ -451,4 +465,28 @@ Module Make (N:NType) <: ZType.
  rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith.
  Qed.
 
+ Definition even z :=
+  match z with
+   | Pos n => N.even n
+   | Neg n => N.even n
+  end.
+
+ Definition odd z :=
+  match z with
+   | Pos n => N.odd n
+   | Neg n => N.odd n
+  end.
+
+ Lemma spec_even : forall z, even z = Zeven_bool (to_Z z).
+ Proof.
+  intros [n|n]; simpl; rewrite N.spec_even; trivial.
+  destruct (N.to_Z n) as [|p|p]; now try destruct p.
+ Qed.
+
+ Lemma spec_odd : forall z, odd z = Zodd_bool (to_Z z).
+ Proof.
+  intros [n|n]; simpl; rewrite N.spec_odd; trivial.
+  destruct (N.to_Z n) as [|p|p]; now try destruct p.
+ Qed.
+
 End Make.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index e50eac17a..28a37abf8 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,10 +10,40 @@
 
 
 Require Import ZAxioms ZProperties.
-Require Import BinInt Zcompare Zorder ZArith_dec Zbool.
+Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven.
 
 Local Open Scope Z_scope.
 
+(** An alternative Zpow *)
+
+(** The Zpow is extensionnaly equal to Zpower in ZArith, but not
+    convertible with it. This Zpow uses a logarithmic number of
+    multiplications instead of a linear one. We should try someday to
+    replace Zpower with this Zpow.
+*)
+
+Definition Zpow n m :=
+  match m with
+    | Z0 => 1
+    | Zpos p => Piter_op Zmult p n
+    | Zneg p => 0
+  end.
+
+Lemma Zpow_0_r : forall n, Zpow n 0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma Zpow_succ_r : forall a b, 0<=b -> Zpow a (Zsucc b) = a * Zpow a b.
+Proof.
+ intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
+ now rewrite Zmult_1_r.
+ rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
+Qed.
+
+Lemma Zpow_neg : forall a b, b<0 -> Zpow a b = 0.
+Proof.
+ now destruct b.
+Qed.
+
 Theorem Z_bi_induction :
   forall A : Z -> Prop, Proper (eq ==> iff) A ->
     A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
@@ -24,11 +54,10 @@ intros; rewrite <- Zsucc_succ'. now apply -> AS.
 intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS.
 Qed.
 
-
-(** * Implementation of [ZAxiomsSig] by [BinInt.Z] *)
+(** * Implementation of [ZAxiomsMiniSig] by [BinInt.Z] *)
 
 Module Z
- <: ZAxiomsExtSig <: UsualOrderedTypeFull <: TotalOrder
+ <: ZAxiomsSig <: UsualOrderedTypeFull <: TotalOrder
  <: UsualDecidableTypeFull.
 
 Definition t := Z.
@@ -110,13 +139,36 @@ Definition sgn_null := Zsgn_0.
 Definition sgn_pos := Zsgn_1.
 Definition sgn_neg := Zsgn_m1.
 
+(** Even and Odd *)
+
+Definition Even n := exists m, n=2*m.
+Definition Odd n := exists m, n=2*m+1.
+
+Lemma even_spec n : Zeven_bool n = true <-> Even n.
+Proof. rewrite Zeven_bool_iff. exact (Zeven_ex_iff n). Qed.
+
+Lemma odd_spec n : Zodd_bool n = true <-> Odd n.
+Proof. rewrite Zodd_bool_iff. exact (Zodd_ex_iff n). Qed.
+
+Definition even := Zeven_bool.
+Definition odd := Zodd_bool.
+
+(** Power *)
+
+Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow.
+
+Definition pow_0_r := Zpow_0_r.
+Definition pow_succ_r := Zpow_succ_r.
+Definition pow_neg := Zpow_neg.
+Definition pow := Zpow.
+
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
 Definition eq := (@eq Z).
 
 (** Now the generic properties. *)
 
-Include ZPropFunct
+Include ZProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End Z.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 00ee19b3a..7df1871e1 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -8,16 +8,17 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Import NProperties. (* The most complete file for N *)
-Require Export ZProperties. (* The most complete file for Z *)
+Require Import NSub ZAxioms.
 Require Export Ring.
 
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
 Open Local Scope pair_scope.
 
-Module ZPairsAxiomsMod (Import N : NAxiomsSig) <: ZAxiomsSig.
-Module Import NPropMod := NPropFunct N. (* Get all properties of N *)
+Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig.
+ Module Import NProp.
+   Include NSubProp N.
+ End NProp.
 
 Delimit Scope NScope with N.
 Bind Scope NScope with N.t.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 021f4b1bf..b33ed5f8e 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -46,8 +46,9 @@ Module Type ZType.
  Parameter opp : t -> t.
  Parameter mul : t -> t -> t.
  Parameter square : t -> t.
- Parameter power_pos : t -> positive -> t.
- Parameter power : t -> N -> t.
+ Parameter pow_pos : t -> positive -> t.
+ Parameter pow_N : t -> N -> t.
+ Parameter pow : t -> t -> t.
  Parameter sqrt : t -> t.
  Parameter div_eucl : t -> t -> t * t.
  Parameter div : t -> t -> t.
@@ -55,6 +56,8 @@ Module Type ZType.
  Parameter gcd : t -> t -> t.
  Parameter sgn : t -> t.
  Parameter abs : t -> t.
+ Parameter even : t -> bool.
+ Parameter odd : t -> bool.
 
  Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
  Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
@@ -70,8 +73,9 @@ Module Type ZType.
  Parameter spec_opp: forall x, [opp x] = - [x].
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
  Parameter spec_square: forall x, [square x] = [x] *  [x].
- Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
- Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
+ Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
+ Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
+ Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
  Parameter spec_sqrt: forall x, 0 <= [x] ->
    [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
  Parameter spec_div_eucl: forall x y,
@@ -81,6 +85,8 @@ Module Type ZType.
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b).
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
+ Parameter spec_even : forall x, even x = Zeven_bool [x].
+ Parameter spec_odd : forall x, odd x = Zodd_bool [x].
 
 End ZType.
 
@@ -91,6 +97,7 @@ Module Type ZType_Notation (Import Z:ZType).
  Infix "+" := add.
  Infix "-" := sub.
  Infix "*" := mul.
+ Infix "^" := pow.
  Notation "- x" := (opp x).
  Infix "<=" := le.
  Infix "<" := lt.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 48cf9e868..90bda6343 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith ZAxioms ZDivFloor ZSig.
+Require Import ZArith Nnat ZAxioms ZDivFloor ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig]
 
@@ -20,6 +20,7 @@ Hint Rewrite
  spec_0 spec_1 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
+ spec_pow spec_even spec_odd
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -188,13 +189,15 @@ Qed.
 
 (** Part specific to integers, not natural numbers *)
 
-Program Instance opp_wd : Proper (eq ==> eq) opp.
-
 Theorem succ_pred : forall n, succ (pred n) == n.
 Proof.
 intros. zify. auto with zarith.
 Qed.
 
+(** Opp *)
+
+Program Instance opp_wd : Proper (eq ==> eq) opp.
+
 Theorem opp_0 : - 0 == 0.
 Proof.
 intros. zify. auto with zarith.
@@ -205,6 +208,8 @@ Proof.
 intros. zify. auto with zarith.
 Qed.
 
+(** Abs / Sgn *)
+
 Theorem abs_eq : forall n, 0 <= n -> abs n == n.
 Proof.
 intros n. zify. omega with *.
@@ -230,6 +235,67 @@ Proof.
 intros n. zify. omega with *.
 Qed.
 
+(** Power *)
+
+Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
+
+Local Notation "1" := (succ 0).
+Local Notation "2" := (succ 1).
+
+Lemma pow_0_r : forall a, a^0 == 1.
+Proof.
+ intros. now zify.
+Qed.
+
+Lemma pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b.
+Proof.
+ intros a b. zify. intros Hb.
+ rewrite Zpower_exp; auto with zarith.
+ simpl. unfold Zpower_pos; simpl. ring.
+Qed.
+
+Lemma pow_neg : forall a b, b<0 -> a^b == 0.
+Proof.
+ intros a b. zify. intros Hb.
+ destruct [b]; reflexivity || discriminate.
+Qed.
+
+Lemma pow_pow_N : forall a b, 0<=b -> a^b == pow_N a (Zabs_N (to_Z b)).
+Proof.
+ intros a b. zify. intros Hb.
+ now rewrite spec_pow_N, Z_of_N_abs, Zabs_eq.
+Qed.
+
+Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p).
+Proof.
+ intros a b. red. now rewrite spec_pow_N, spec_pow_pos.
+Qed.
+
+(** Even / Odd *)
+
+Definition Even n := exists m, n == 2*m.
+Definition Odd n := exists m, n == 2*m+1.
+
+Lemma even_spec : forall n, even n = true <-> Even n.
+Proof.
+ intros n. unfold Even. zify.
+ rewrite Zeven_bool_iff, Zeven_ex_iff.
+ split; intros (m,Hm).
+ exists (of_Z m). now zify.
+ exists [m]. revert Hm. now zify.
+Qed.
+
+Lemma odd_spec : forall n, odd n = true <-> Odd n.
+Proof.
+ intros n. unfold Odd. zify.
+ rewrite Zodd_bool_iff, Zodd_ex_iff.
+ split; intros (m,Hm).
+ exists (of_Z m). now zify.
+ exists [m]. revert Hm. now zify.
+Qed.
+
+(** Div / Mod *)
+
 Program Instance div_wd : Proper (eq==>eq==>eq) div.
 Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.