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

10 files changed, 425 insertions, 35 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index bceea42b7..7d7cc4ac5 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -10,8 +10,7 @@
 
 Require Import NZAxioms NZBase.
 
-Module Type NZAddPropSig
- (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
+Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ).
 
 Hint Rewrite
  pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz.
@@ -76,8 +75,7 @@ Qed.
 
 Theorem add_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p).
 Proof.
-intros n m p q.
-rewrite 2 add_assoc, add_shuffle0, add_cancel_r. apply add_shuffle0.
+intros n m p q. rewrite (add_comm p). apply add_shuffle1.
 Qed.
 
 Theorem sub_1_r : forall n, n - 1 == P n.
@@ -85,4 +83,4 @@ Proof.
 intro n; now nzsimpl.
 Qed.
 
-End NZAddPropSig.
+End NZAddProp.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index b715b4b00..3aa6f41d3 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -10,8 +10,8 @@
 
 Require Import NZAxioms NZBase NZMul NZOrder.
 
-Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
+Module Type NZAddOrderProp (Import NZ : NZOrdAxiomsSig').
+Include NZBaseProp NZ <+ NZMulProp NZ <+ NZOrderProp NZ.
 
 Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
 Proof.
@@ -147,5 +147,22 @@ Proof.
 intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
-End NZAddOrderPropSig.
+(** Substraction *)
+
+(** We can prove the existence of a subtraction of any number by
+    a smaller one *)
+
+Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p.
+Proof.
+ intros n m H. apply le_ind with (4:=H). solve_predicate_wd.
+ exists 0; nzsimpl; split; order.
+ clear m H. intros m H (p & EQ & LE). exists (S p).
+  split. nzsimpl. now apply succ_wd. now apply le_le_succ_r.
+Qed.
+
+(** For the moment, it doesn't seem possible to relate
+    this existing subtraction with [sub].
+*)
+
+End NZAddOrderProp.
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index d2437e354..a86fec3fd 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -10,7 +10,7 @@
 
 Require Import NZAxioms.
 
-Module Type NZBasePropSig (Import NZ : NZDomainSig').
+Module Type NZBaseProp (Import NZ : NZDomainSig').
 
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
 
@@ -83,5 +83,5 @@ Tactic Notation "nzinduct" ident(n) :=
 Tactic Notation "nzinduct" ident(n) constr(u) :=
   induction_maker n ltac:(apply central_induction with (z := u)).
 
-End NZBasePropSig.
+End NZBaseProp.
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 75f0206f8..3b9720f32 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -45,11 +45,10 @@ Module Type NZDiv (NZ:NZOrdAxiomsSig)
 
 Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ.
 
-Module NZDivPropFunct
+Module NZDivProp
  (Import NZ : NZOrdAxiomsSig')
- (Import NZP : NZMulOrderPropSig NZ)
- (Import NZD : NZDiv' NZ)
-.
+ (Import NZP : NZMulOrderProp NZ)
+ (Import NZD : NZDiv' NZ).
 
 (** Uniqueness theorems *)
 
@@ -538,5 +537,5 @@ Proof.
  rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order.
 Qed.
 
-End NZDivPropFunct.
+End NZDivProp.
 
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index f07c55524..a26e93d76 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -305,7 +305,7 @@ End NZOfNat.
 
 Module NZOfNatOrd (Import NZ:NZOrdSig').
 Include NZOfNat NZ.
-Include NZOrderPropFunct NZ.
+Include NZBaseProp NZ <+ NZOrderProp NZ.
 Local Open Scope ofnat.
 
 Theorem ofnat_S_gt_0 :
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index a87d6ac62..55ec3f30e 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -10,9 +10,8 @@
 
 Require Import NZAxioms NZBase NZAdd.
 
-Module Type NZMulPropSig
- (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
-Include NZAddPropSig NZ NZBase.
+Module Type NZMulProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ).
+Include NZAddProp NZ NZBase.
 
 Theorem mul_0_r : forall n, n * 0 == 0.
 Proof.
@@ -65,4 +64,19 @@ Proof.
 intro n. now nzsimpl.
 Qed.
 
-End NZMulPropSig.
+Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m.
+Proof.
+intros n m p. now rewrite <- 2 mul_assoc, (mul_comm m).
+Qed.
+
+Theorem mul_shuffle1 : forall n m p q, (n * m) * (p * q) == (n * p) * (m * q).
+Proof.
+intros n m p q. now rewrite 2 mul_assoc, (mul_shuffle0 n).
+Qed.
+
+Theorem mul_shuffle2 : forall n m p q, (n * m) * (p * q) == (n * q) * (m * p).
+Proof.
+intros n m p q. rewrite (mul_comm p). apply mul_shuffle1.
+Qed.
+
+End NZMulProp.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 414931ba8..530044ab0 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -11,8 +11,8 @@
 Require Import NZAxioms.
 Require Import NZAddOrder.
 
-Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig').
-Include NZAddOrderPropSig NZ.
+Module Type NZMulOrderProp (Import NZ : NZOrdAxiomsSig').
+Include NZAddOrderProp NZ.
 
 Theorem mul_lt_pred :
   forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
@@ -302,4 +302,4 @@ rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l.
 apply add_pos_pos; now apply lt_0_1.
 Qed.
 
-End NZMulOrderPropSig.
+End NZMulOrderProp.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 8fdf8b47e..93201964e 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -10,8 +10,8 @@
 
 Require Import NZAxioms NZBase Decidable OrdersTac.
 
-Module Type NZOrderPropSig
- (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ).
+Module Type NZOrderProp
+ (Import NZ : NZOrdSig')(Import NZBase : NZBaseProp NZ).
 
 Instance le_wd : Proper (eq==>eq==>iff) le.
 Proof.
@@ -357,6 +357,13 @@ intros z n H; apply lt_exists_pred_strong with (z := z) (n := n).
 assumption. apply le_refl.
 Qed.
 
+Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n.
+Proof.
+ intros z n H.
+ destruct (lt_exists_pred _ _ H) as (n' & EQ & LE).
+ rewrite EQ. now rewrite pred_succ.
+Qed.
+
 (** Stronger variant of induction with assumptions n >= 0 (n < 0)
 in the induction step *)
 
@@ -557,7 +564,7 @@ apply right_induction with (S n); [assumption | | now apply <- le_succ_l].
 intros; apply H2; try assumption. now apply -> le_succ_l.
 Qed.
 
-(** Elimintation principle for <= *)
+(** Elimination principle for <= *)
 
 Theorem le_ind : forall (n : t),
   A n ->
@@ -628,15 +635,12 @@ Qed.
 
 End WF.
 
-End NZOrderPropSig.
-
-Module NZOrderPropFunct (NZ : NZOrdSig) :=
- NZBasePropSig NZ <+ NZOrderPropSig NZ.
+End NZOrderProp.
 
 (** If we have moreover a [compare] function, we can build
     an [OrderedType] structure. *)
 
-Module NZOrderedTypeFunct (NZ : NZDecOrdSig')
-  <: DecidableTypeFull <: OrderedTypeFull :=
- NZ <+ NZOrderPropFunct <+ Compare2EqBool <+ HasEqBool2Dec.
+Module NZOrderedType (NZ : NZDecOrdSig')
+ <: DecidableTypeFull <: OrderedTypeFull
+ := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
 
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
new file mode 100644
index 000000000..cbc286fbb
--- /dev/null
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -0,0 +1,358 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Power Function *)
+
+Require Import NZAxioms NZMulOrder.
+
+(** Interface of a power function, then its specification on naturals *)
+
+Module Type Pow (Import T:Typ).
+ Parameters Inline pow : t -> t -> t.
+End Pow.
+
+Module Type PowNotation (T:Typ)(Import NZ:Pow T).
+ Infix "^" := pow.
+End PowNotation.
+
+Module Type Pow' (T:Typ) := Pow T <+ PowNotation T.
+
+Module Type NZPowSpec (Import NZ : NZOrdAxiomsSig')(Import P : Pow' NZ).
+ Declare Instance pow_wd : Proper (eq==>eq==>eq) pow.
+ Axiom pow_0_r : forall a, a^0 == 1.
+ Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b.
+End NZPowSpec.
+
+Module Type NZPow (NZ:NZOrdAxiomsSig) := Pow NZ <+ NZPowSpec NZ.
+Module Type NZPow' (NZ:NZOrdAxiomsSig) := Pow' NZ <+ NZPowSpec NZ.
+
+(** Derived properties of power *)
+
+Module NZPowProp
+ (Import NZ : NZOrdAxiomsSig')
+ (Import NZP : NZMulOrderProp NZ)
+ (Import NZP' : NZPow' NZ).
+
+Hint Rewrite pow_0_r pow_succ_r : nz.
+
+Lemma lt_0_2 : 0 < 2.
+Proof.
+ apply lt_succ_r, le_0_1.
+Qed.
+
+Ltac order' := generalize lt_0_1 lt_0_2; order.
+
+(** Power and basic constants *)
+
+Lemma pow_0_l : forall a, 0<a -> 0^a == 0.
+Proof.
+ intros a Ha.
+ destruct (lt_exists_pred _ _ Ha) as (a' & EQ & Ha').
+ rewrite EQ. now nzsimpl.
+Qed.
+
+Lemma pow_1_r : forall a, a^1 == a.
+Proof.
+ intros. now nzsimpl.
+Qed.
+
+Lemma pow_1_l : forall a, 0<=a -> 1^a == 1.
+Proof.
+ apply le_ind; intros. solve_predicate_wd.
+ now nzsimpl.
+ now nzsimpl.
+Qed.
+
+Hint Rewrite pow_1_l : nz.
+
+Lemma pow_2_r : forall a, a^2 == a*a.
+Proof.
+ intros. nzsimpl; order'.
+Qed.
+
+(** Power and addition, multiplication *)
+
+Lemma pow_add_r : forall a b c, 0<=b -> 0<=c ->
+  a^(b+c) == a^b * a^c.
+Proof.
+ intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ now nzsimpl.
+ clear b Hb. intros b Hb IH Hc.
+ nzsimpl; trivial.
+ rewrite IH; trivial. apply mul_assoc.
+ now apply add_nonneg_nonneg.
+Qed.
+
+Lemma pow_mul_l : forall a b c, 0<=c ->
+  (a*b)^c == a^c * b^c.
+Proof.
+ intros a b c Hc. apply le_ind with (4:=Hc). solve_predicate_wd.
+ now nzsimpl.
+ clear c Hc. intros c Hc IH.
+ nzsimpl; trivial.
+ rewrite IH; trivial. apply mul_shuffle1.
+Qed.
+
+Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c ->
+  a^(b*c) == (a^b)^c.
+Proof.
+ intros a b c Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ intros. now nzsimpl.
+ clear b Hb. intros b Hb IH Hc.
+ nzsimpl; trivial.
+ rewrite pow_add_r, IH, pow_mul_l; trivial. apply mul_comm.
+ now apply mul_nonneg_nonneg.
+Qed.
+
+(** Positivity *)
+
+Lemma pow_nonneg_nonneg : forall a b, 0<=a -> 0<=b -> 0<=a^b.
+Proof.
+ intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ nzsimpl; order'.
+ clear b Hb. intros b Hb IH.
+ nzsimpl; trivial. now apply mul_nonneg_nonneg.
+Qed.
+
+Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b.
+Proof.
+ intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ nzsimpl; order'.
+ clear b Hb. intros b Hb IH.
+ nzsimpl; trivial. now apply mul_pos_pos.
+Qed.
+
+(** Monotonicity *)
+
+Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c.
+Proof.
+ intros a b c Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
+ intros (Ha,H). nzsimpl; trivial; order.
+ clear c Hc. intros c Hc IH (Ha,H).
+ nzsimpl; try order.
+ apply mul_lt_mono_nonneg; trivial.
+ apply pow_nonneg_nonneg; try order.
+ apply IH. now split.
+Qed.
+
+Lemma pow_le_mono_l : forall a b c, 0<=c -> 0<=a<=b -> a^c <= b^c.
+Proof.
+ intros a b c Hc (Ha,H).
+ apply lt_eq_cases in Hc; destruct Hc as [Hc|Hc]; [|rewrite <- Hc].
+ apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H].
+ apply lt_le_incl, pow_lt_mono_l; now try split.
+ now nzsimpl.
+Qed.
+
+Lemma pow_gt_1 : forall a b, 1<a -> 0<b -> 1<a^b.
+Proof.
+ intros a b Ha Hb. rewrite <- (pow_1_l b) by order.
+ apply pow_lt_mono_l; try split; order'.
+Qed.
+
+Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=b<c -> a^b < a^c.
+Proof.
+ intros a b c Ha (Hb,H).
+ assert (H' : b<=c) by order.
+ destruct (le_exists_sub _ _ H') as (d & EQ & Hd).
+ rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1.
+ apply mul_lt_mono_pos_r.
+ apply pow_pos_nonneg; order'.
+ apply pow_gt_1; trivial.
+ apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial.
+  rewrite <- EQ' in *. rewrite add_0_l in EQ. 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 -> 0<=b<=c -> a^b <= a^c.
+Proof.
+ intros a b c Ha (Hb,H).
+ apply le_succ_l in Ha.
+ apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
+ apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
+ apply lt_le_incl, pow_lt_mono_r; now try split.
+ nzsimpl; order.
+Qed.
+
+Lemma pow_le_mono : forall a b c d, 0<a<=c -> 0<=b<=d ->
+ a^b <= c^d.
+Proof.
+ intros. transitivity (a^d).
+ apply pow_le_mono_r; intuition order.
+ apply pow_le_mono_l; intuition order.
+Qed.
+
+Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
+ a^b < c^d.
+Proof.
+ intros a b c d (Ha,Hac) (Hb,Hbd).
+ apply le_succ_l in Ha.
+ apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
+ transitivity (a^d).
+ apply pow_lt_mono_r; intuition order.
+ apply pow_lt_mono_l; try split; order'.
+ nzsimpl; try order. apply pow_gt_1; order.
+Qed.
+
+(** Injectivity *)
+
+Lemma pow_inj_l : forall a b c, 0<=a -> 0<=b -> 0<c ->
+ a^c == b^c -> a == b.
+Proof.
+ intros a b c Ha Hb Hc EQ.
+ destruct (lt_trichotomy a b) as [LT|[EQ'|GT]]; trivial.
+ assert (a^c < b^c) by (apply pow_lt_mono_l; try split; trivial).
+ order.
+ assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
+ order.
+Qed.
+
+Lemma pow_inj_r : forall a b c, 1<a -> 0<=b -> 0<=c ->
+ a^b == a^c -> b == c.
+Proof.
+ intros a b c Ha Hb Hc EQ.
+ destruct (lt_trichotomy b c) as [LT|[EQ'|GT]]; trivial.
+ assert (a^b < a^c) by (apply pow_lt_mono_r; try split; trivial).
+ order.
+ assert (a^c < a^b) by (apply pow_lt_mono_r; try split; trivial).
+ order.
+Qed.
+
+(** Monotonicity results, both ways *)
+
+Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
+  (a<b <-> a^c < b^c).
+Proof.
+ intros a b c Ha Hb Hc.
+ split; intro LT.
+ apply pow_lt_mono_l; try split; trivial.
+ destruct (le_gt_cases b a) as [LE|GT]; trivial.
+ assert (b^c <= a^c) by (apply pow_le_mono_l; try split; order).
+ order.
+Qed.
+
+Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
+  (a<=b <-> a^c <= b^c).
+Proof.
+ intros a b c Ha Hb Hc.
+ split; intro LE.
+ apply pow_le_mono_l; try split; trivial. order.
+ destruct (le_gt_cases a b) as [LE'|GT]; trivial.
+ assert (b^c < a^c) by (apply pow_lt_mono_l; try split; trivial).
+ order.
+Qed.
+
+Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c ->
+  (b<c <-> a^b < a^c).
+Proof.
+ intros a b c Ha Hb Hc.
+ split; intro LT.
+ apply pow_lt_mono_r; try split; trivial.
+ destruct (le_gt_cases c b) as [LE|GT]; trivial.
+ assert (a^c <= a^b) by (apply pow_le_mono_r; try split; order').
+ order.
+Qed.
+
+Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c ->
+  (b<=c <-> a^b <= a^c).
+Proof.
+ intros a b c Ha Hb Hc.
+ split; intro LE.
+ apply pow_le_mono_r; try split; trivial. order'.
+ destruct (le_gt_cases b c) as [LE'|GT]; trivial.
+ assert (a^c < a^b) by (apply pow_lt_mono_r; try split; order').
+ order.
+Qed.
+
+(** For any a>1, the a^x function is above the identity function *)
+
+Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b.
+Proof.
+ intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
+ nzsimpl. order'.
+ clear b Hb. intros b Hb IH. nzsimpl; trivial.
+ rewrite <- !le_succ_l in *.
+ transitivity (2*(S b)).
+  nzsimpl. rewrite <- 2 succ_le_mono.
+  rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
+ apply mul_le_mono_nonneg; trivial.
+ order'.
+ now apply lt_le_incl, lt_succ_r.
+Qed.
+
+(** Someday, we should say something about the full Newton formula.
+    In the meantime, we can at least provide some inequalities about
+    (a+b)^c.
+*)
+
+Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c ->
+  a^c + b^c <= (a+b)^c.
+Proof.
+ intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
+ nzsimpl; order.
+ clear c Hc. intros c Hc IH.
+ assert (0<=c) by order'.
+ nzsimpl; trivial.
+ transitivity ((a+b)*(a^c + b^c)).
+ rewrite mul_add_distr_r, !mul_add_distr_l.
+ apply add_le_mono.
+ rewrite <- add_0_r at 1. apply add_le_mono_l.
+  apply mul_nonneg_nonneg; trivial.
+  apply pow_nonneg_nonneg; trivial.
+ rewrite <- add_0_l at 1. apply add_le_mono_r.
+  apply mul_nonneg_nonneg; trivial.
+  apply pow_nonneg_nonneg; trivial.
+ apply mul_le_mono_nonneg_l; trivial.
+ now apply add_nonneg_nonneg.
+Qed.
+
+(** This upper bound can also be seen as a convexity proof for x^c :
+    image of (a+b)/2 is below the middle of the images of a and b
+*)
+
+Lemma pow_add_upper : forall a b c, 0<=a -> 0<=b -> 0<c ->
+  (a+b)^c <= 2^(pred c) * (a^c + b^c).
+Proof.
+ assert (aux : forall a b c, 0<=a<=b -> 0<c ->
+         (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)).
+ (* begin *)
+  intros a b c (Ha,H) Hc.
+  rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl.
+  rewrite <- !add_assoc. apply add_le_mono_l.
+  rewrite !add_assoc. apply add_le_mono_r.
+  destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
+  rewrite EQ.
+  rewrite 2 mul_add_distr_r.
+  rewrite !add_assoc. apply add_le_mono_r.
+  rewrite add_comm. apply add_le_mono_l.
+  apply mul_le_mono_nonneg_l; trivial.
+  apply pow_le_mono_l; try split; order.
+ (* end *)
+ intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). solve_predicate_wd.
+ nzsimpl; order.
+ clear c Hc. intros c Hc IH.
+ assert (0<=c) by order.
+ nzsimpl; trivial.
+ transitivity ((a+b)*(2^(pred c) * (a^c + b^c))).
+ apply mul_le_mono_nonneg_l; trivial.
+ now apply add_nonneg_nonneg.
+ rewrite mul_assoc. rewrite (mul_comm (a+b)).
+ assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order').
+ assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l).
+ assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl; order).
+ rewrite EQ', <- !mul_assoc.
+ apply mul_le_mono_nonneg_l.
+ apply pow_nonneg_nonneg; order'.
+ destruct (le_gt_cases a b).
+ apply aux; try split; order'.
+ rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)).
+ apply aux; try split; order'.
+Qed.
+
+End NZPowProp.
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
index 5ef304606..13c262337 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.v
@@ -11,8 +11,8 @@
 Require Export NZAxioms NZMulOrder.
 
 (** This functor summarizes all known facts about NZ.
-    For the moment it is only an alias to [NZMulOrderPropFunct], which
+    For the moment it is only an alias to [NZMulOrderProp], which
     subsumes all others.
 *)
 
-Module Type NZPropFunct := NZMulOrderPropSig.
+Module Type NZProp := NZMulOrderProp.