Imported Upstream version 8.4~betaupstream/8.4_beta

16 files changed, 3106 insertions, 320 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 782619f0..8bed3027 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,16 +8,15 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NZAdd.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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.
+Hint Rewrite one_succ two_succ : nz'.
 Ltac nzsimpl := autorewrite with nz.
+Ltac nzsimpl' := autorewrite with nz nz'.
 
 Theorem add_0_r : forall n, n + 0 == n.
 Proof.
@@ -31,6 +30,11 @@ intros n m; nzinduct n. now nzsimpl.
 intro. nzsimpl. now rewrite succ_inj_wd.
 Qed.
 
+Theorem add_succ_comm : forall n m, S n + m == n + S m.
+Proof.
+intros n m. now rewrite add_succ_r, add_succ_l.
+Qed.
+
 Hint Rewrite add_0_r add_succ_r : nz.
 
 Theorem add_comm : forall n m, n + m == m + n.
@@ -41,14 +45,16 @@ Qed.
 
 Theorem add_1_l : forall n, 1 + n == S n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
 Theorem add_1_r : forall n, n + 1 == S n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
+Hint Rewrite add_1_l add_1_r : nz.
+
 Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
 intros n m p; nzinduct n. now nzsimpl.
@@ -78,13 +84,19 @@ 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 add_shuffle3 : forall n m p, n + (m + p) == m + (n + p).
+Proof.
+intros n m p. now rewrite add_comm, <- add_assoc, (add_comm p).
 Qed.
 
 Theorem sub_1_r : forall n, n - 1 == P n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
-End NZAddPropSig.
+Hint Rewrite sub_1_r : nz.
+
+End NZAddProp.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index ed56cd8f..ee03e5f9 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,12 +8,10 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NZAddOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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.
@@ -30,7 +28,7 @@ Theorem add_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply lt_trans with (m + p);
-[now apply -> add_lt_mono_r | now apply -> add_lt_mono_l].
+[now apply add_lt_mono_r | now apply add_lt_mono_l].
 Qed.
 
 Theorem add_le_mono_l : forall n m p, n <= m <-> p + n <= p + m.
@@ -48,21 +46,21 @@ Theorem add_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
 Proof.
 intros n m p q H1 H2.
 apply le_trans with (m + p);
-[now apply -> add_le_mono_r | now apply -> add_le_mono_l].
+[now apply add_le_mono_r | now apply add_le_mono_l].
 Qed.
 
 Theorem add_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply lt_le_trans with (m + p);
-[now apply -> add_lt_mono_r | now apply -> add_le_mono_l].
+[now apply add_lt_mono_r | now apply add_le_mono_l].
 Qed.
 
 Theorem add_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
 apply le_lt_trans with (m + p);
-[now apply -> add_le_mono_r | now apply -> add_lt_mono_l].
+[now apply add_le_mono_r | now apply add_lt_mono_l].
 Qed.
 
 Theorem add_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n + m.
@@ -149,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_proper.
+ exists 0; nzsimpl; split; order.
+ clear m H. intros m H (p & EQ & LE). exists (S p).
+  split. nzsimpl. now f_equiv. 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/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 33236cde..fcd98787 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,8 +8,6 @@
 
 (** Initial Author : Evgeny Makarov, INRIA, 2007 *)
 
-(*i $Id: NZAxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Equalities Orders NumPrelude GenericMinMax.
 
 (** Axiomatization of a domain with zero, successor, predecessor,
@@ -20,7 +18,7 @@ Require Export Equalities Orders NumPrelude GenericMinMax.
 *)
 
 Module Type ZeroSuccPred (Import T:Typ).
- Parameter Inline zero : t.
+ Parameter Inline(20) zero : t.
  Parameters Inline succ pred : t -> t.
 End ZeroSuccPred.
 
@@ -28,8 +26,6 @@ Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T).
  Notation "0" := zero.
  Notation S := succ.
  Notation P := pred.
- Notation "1" := (S 0).
- Notation "2" := (S 1).
 End ZeroSuccPredNotation.
 
 Module Type ZeroSuccPred' (T:Typ) :=
@@ -44,9 +40,33 @@ Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E).
     A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
 End IsNZDomain.
 
-Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain.
-Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain.
+(** Axiomatization of some more constants
+
+    Simply denoting "1" for (S 0) and so on works ok when implementing
+    by nat, but leaves some (Nsucc N0) when implementing by N.
+*)
+
+Module Type OneTwo (Import T:Typ).
+ Parameter Inline(20) one two : t.
+End OneTwo.
 
+Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T).
+ Notation "1" := one.
+ Notation "2" := two.
+End OneTwoNotation.
+
+Module Type OneTwo' (T:Typ) := OneTwo T <+ OneTwoNotation T.
+
+Module Type IsOneTwo (E:Eq')(Z:ZeroSuccPred' E)(O:OneTwo' E).
+ Import E Z O.
+ Axiom one_succ : 1 == S 0.
+ Axiom two_succ : 2 == S 1.
+End IsOneTwo.
+
+Module Type NZDomainSig :=
+ EqualityType <+ ZeroSuccPred <+ IsNZDomain <+ OneTwo <+ IsOneTwo.
+Module Type NZDomainSig' :=
+ EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo.
 
 (** Axiomatization of basic operations : [+] [-] [*] *)
 
@@ -117,3 +137,9 @@ Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare.
 Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare.
 Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare.
 
+(** A square function *)
+
+Module Type NZSquare (Import NZ : NZBasicFunsSig').
+ Parameter Inline square : t -> t.
+ Axiom square_spec : forall n, square n == n * n.
+End NZSquare.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 119f8265..65b64635 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,11 +8,14 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NZBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import NZAxioms.
 
-Module Type NZBasePropSig (Import NZ : NZDomainSig').
+Module Type NZBaseProp (Import NZ : NZDomainSig').
+
+(** An artificial scope meant to be substituted later *)
+
+Delimit Scope abstract_scope with abstract.
+Bind Scope abstract_scope with t.
 
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
 
@@ -50,7 +53,7 @@ Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
 Proof.
 intros; split.
 apply succ_inj.
-apply succ_wd.
+intros. now f_equiv.
 Qed.
 
 Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
@@ -63,7 +66,7 @@ left-inverse to the successor at this point *)
 
 Section CentralInduction.
 
-Variable A : predicate t.
+Variable A : t -> Prop.
 Hypothesis A_wd : Proper (eq==>iff) A.
 
 Theorem central_induction :
@@ -72,7 +75,7 @@ Theorem central_induction :
       forall n, A n.
 Proof.
 intros z Base Step; revert Base; pattern z; apply bi_induction.
-solve_predicate_wd.
+solve_proper.
 intro; now apply bi_induction.
 intro; pose proof (Step n); tauto.
 Qed.
@@ -85,5 +88,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/NZBits.v b/theories/Numbers/NatInt/NZBits.v
new file mode 100644
index 00000000..dc97eeb1
--- /dev/null
+++ b/theories/Numbers/NatInt/NZBits.v
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  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 NZAxioms NZMulOrder NZParity NZPow NZDiv NZLog.
+
+(** Axiomatization of some bitwise operations *)
+
+Module Type Bits (Import A : Typ).
+ Parameter Inline testbit : t -> t -> bool.
+ Parameters Inline shiftl shiftr land lor ldiff lxor : t -> t -> t.
+ Parameter Inline div2 : t -> t.
+End Bits.
+
+Module Type BitsNotation (Import A : Typ)(Import B : Bits A).
+ Notation "a .[ n ]" := (testbit a n) (at level 5, format "a .[ n ]").
+ Infix ">>" := shiftr (at level 30, no associativity).
+ Infix "<<" := shiftl (at level 30, no associativity).
+End BitsNotation.
+
+Module Type Bits' (A:Typ) := Bits A <+ BitsNotation A.
+
+Module Type NZBitsSpec
+ (Import A : NZOrdAxiomsSig')(Import B : Bits' A).
+
+ Declare Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
+ Axiom testbit_odd_0 : forall a, (2*a+1).[0] = true.
+ Axiom testbit_even_0 : forall a, (2*a).[0] = false.
+ Axiom testbit_odd_succ : forall a n, 0<=n -> (2*a+1).[S n] = a.[n].
+ Axiom testbit_even_succ : forall a n, 0<=n -> (2*a).[S n] = a.[n].
+ Axiom testbit_neg_r : forall a n, n<0 -> a.[n] = false.
+
+ Axiom shiftr_spec : forall a n m, 0<=m -> (a >> n).[m] = a.[m+n].
+ Axiom shiftl_spec_high : forall a n m, 0<=m -> n<=m -> (a << n).[m] = a.[m-n].
+ Axiom shiftl_spec_low : forall a n m, m<n -> (a << n).[m] = false.
+
+ Axiom land_spec : forall a b n, (land a b).[n] = a.[n] && b.[n].
+ Axiom lor_spec : forall a b n, (lor a b).[n] = a.[n] || b.[n].
+ Axiom ldiff_spec : forall a b n, (ldiff a b).[n] = a.[n] && negb b.[n].
+ Axiom lxor_spec : forall a b n, (lxor a b).[n] = xorb a.[n] b.[n].
+ Axiom div2_spec : forall a, div2 a == a >> 1.
+
+End NZBitsSpec.
+
+Module Type NZBits (A:NZOrdAxiomsSig) := Bits A <+ NZBitsSpec A.
+Module Type NZBits' (A:NZOrdAxiomsSig) := Bits' A <+ NZBitsSpec A.
+
+(** In the functor of properties will also be defined:
+   - [setbit : t -> t -> t ] defined as [lor a (1<<n)].
+   - [clearbit : t -> t -> t ] defined as [ldiff a (1<<n)].
+   - [ones : t -> t], the number with [n] initial true bits,
+     corresponding to [2^n - 1].
+   - a logical complement [lnot]. For integer numbers it will
+     be a [t->t], doing a swap of all bits, while on natural
+     numbers, it will be a bounded complement [t->t->t], swapping
+     only the first [n] bits.
+*)
+
+(** For the moment, no shared properties about NZ here,
+  since properties and proofs for N and Z are quite different *)
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index ba1c171e..bc109ace 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -12,44 +12,36 @@ Require Import NZAxioms NZMulOrder.
 
 (** The first signatures will be common to all divisions over NZ, N and Z *)
 
-Module Type DivMod (Import T:Typ).
+Module Type DivMod (Import A : Typ).
  Parameters Inline div modulo : t -> t -> t.
 End DivMod.
 
-Module Type DivModNotation (T:Typ)(Import NZ:DivMod T).
+Module Type DivModNotation (A : Typ)(Import B : DivMod A).
  Infix "/" := div.
  Infix "mod" := modulo (at level 40, no associativity).
 End DivModNotation.
 
-Module Type DivMod' (T:Typ) := DivMod T <+ DivModNotation T.
+Module Type DivMod' (A : Typ) := DivMod A <+ DivModNotation A.
 
-Module Type NZDivCommon (Import NZ : NZAxiomsSig')(Import DM : DivMod' NZ).
+Module Type NZDivSpec (Import A : NZOrdAxiomsSig')(Import B : DivMod' A).
  Declare Instance div_wd : Proper (eq==>eq==>eq) div.
  Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
-End NZDivCommon.
+ Axiom mod_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
+End NZDivSpec.
 
 (** The different divisions will only differ in the conditions
-    they impose on [modulo]. For NZ, we only describe behavior
-    on positive numbers.
-
-    NB: This axiom would also be true for N and Z, but redundant.
+    they impose on [modulo]. For NZ, we have only described the
+    behavior on positive numbers.
 *)
 
-Module Type NZDivSpecific (Import NZ : NZOrdAxiomsSig')(Import DM : DivMod' NZ).
- Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
-End NZDivSpecific.
-
-Module Type NZDiv (NZ:NZOrdAxiomsSig)
- := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ.
+Module Type NZDiv (A : NZOrdAxiomsSig) := DivMod A <+ NZDivSpec A.
+Module Type NZDiv' (A : NZOrdAxiomsSig) := NZDiv A <+ DivModNotation A.
 
-Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ.
-
-Module NZDivPropFunct
- (Import NZ : NZOrdAxiomsSig')
- (Import NZP : NZMulOrderPropSig NZ)
- (Import NZD : NZDiv' NZ)
-.
+Module Type NZDivProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZDiv' A)
+ (Import C : NZMulOrderProp A).
 
 (** Uniqueness theorems *)
 
@@ -84,7 +76,7 @@ Theorem div_unique:
 Proof.
 intros a b q r Ha (Hb,Hr) EQ.
 destruct (div_mod_unique b q (a/b) r (a mod b)); auto.
-apply mod_bound; order.
+apply mod_bound_pos; order.
 rewrite <- div_mod; order.
 Qed.
 
@@ -94,18 +86,21 @@ Theorem mod_unique:
 Proof.
 intros a b q r Ha (Hb,Hr) EQ.
 destruct (div_mod_unique b q (a/b) r (a mod b)); auto.
-apply mod_bound; order.
+apply mod_bound_pos; order.
 rewrite <- div_mod; order.
 Qed.
 
+Theorem div_unique_exact a b q:
+ 0<=a -> 0<b -> a == b*q -> q == a/b.
+Proof.
+ intros Ha Hb H. apply div_unique with 0; nzsimpl; now try split.
+Qed.
 
 (** A division by itself returns 1 *)
 
 Lemma div_same : forall a, 0<a -> a/a == 1.
 Proof.
-intros. symmetry.
-apply div_unique with 0; intuition; try order.
-now nzsimpl.
+intros. symmetry. apply div_unique_exact; nzsimpl; order.
 Qed.
 
 Lemma mod_same : forall a, 0<a -> a mod a == 0.
@@ -147,9 +142,7 @@ Qed.
 
 Lemma div_1_r: forall a, 0<=a -> a/1 == a.
 Proof.
-intros. symmetry.
-apply div_unique with 0; try split; try order; try apply lt_0_1.
-now nzsimpl.
+intros. symmetry. apply div_unique_exact; nzsimpl; order'.
 Qed.
 
 Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0.
@@ -161,20 +154,19 @@ Qed.
 
 Lemma div_1_l: forall a, 1<a -> 1/a == 0.
 Proof.
-intros; apply div_small; split; auto. apply le_succ_diag_r.
+intros; apply div_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
 Proof.
-intros; apply mod_small; split; auto. apply le_succ_diag_r.
+intros; apply mod_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a.
 Proof.
-intros; symmetry.
-apply div_unique with 0; try split; try order.
+intros; symmetry. apply div_unique_exact; trivial.
 apply mul_nonneg_nonneg; order.
-nzsimpl; apply mul_comm.
+apply mul_comm.
 Qed.
 
 Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0.
@@ -194,7 +186,7 @@ Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a.
 Proof.
 intros. destruct (le_gt_cases b a).
 apply le_trans with b; auto.
-apply lt_le_incl. destruct (mod_bound a b); auto.
+apply lt_le_incl. destruct (mod_bound_pos a b); auto.
 rewrite lt_eq_cases; right.
 apply mod_small; auto.
 Qed.
@@ -216,7 +208,7 @@ Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.
 Proof.
 intros a b (Hb,Hab).
 assert (LE : 0 <= a/b) by (apply div_pos; order).
-assert (MOD : a mod b < b) by (destruct (mod_bound a b); order).
+assert (MOD : a mod b < b) by (destruct (mod_bound_pos a b); order).
 rewrite lt_eq_cases in LE; destruct LE as [LT|EQ]; auto.
 exfalso; revert Hab.
 rewrite (div_mod a b), <-EQ; nzsimpl; order.
@@ -263,7 +255,7 @@ rewrite <- (mul_1_l (a/b)) at 1.
 rewrite <- mul_lt_mono_pos_r; auto.
 apply div_str_pos; auto.
 rewrite <- (add_0_r (b*(a/b))) at 1.
-rewrite <- add_le_mono_l. destruct (mod_bound a b); order.
+rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order.
 Qed.
 
 (** [le] is compatible with a positive division. *)
@@ -282,8 +274,8 @@ apply lt_le_trans with b; auto.
 rewrite (div_mod b c) at 1 by order.
 rewrite <- add_assoc, <- add_le_mono_l.
 apply le_trans with (c+0).
-nzsimpl; destruct (mod_bound b c); order.
-rewrite <- add_le_mono_l. destruct (mod_bound a c); order.
+nzsimpl; destruct (mod_bound_pos b c); order.
+rewrite <- add_le_mono_l. destruct (mod_bound_pos a c); order.
 Qed.
 
 (** The following two properties could be used as specification of div *)
@@ -293,7 +285,7 @@ Proof.
 intros.
 rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order.
 rewrite <- (add_0_r a) at 1.
-rewrite <- add_le_mono_l. destruct (mod_bound a b); order.
+rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order.
 Qed.
 
 Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)).
@@ -302,7 +294,7 @@ intros.
 rewrite (div_mod a b) at 1 by order.
 rewrite (mul_succ_r).
 rewrite <- add_lt_mono_l.
-destruct (mod_bound a b); auto.
+destruct (mod_bound_pos a b); auto.
 Qed.
 
 
@@ -359,7 +351,7 @@ Proof.
  apply mul_le_mono_nonneg_r; try order.
  apply div_pos; order.
  rewrite <- (add_0_r (r*(p/r))) at 1.
- rewrite <- add_le_mono_l. destruct (mod_bound p r); order.
+ rewrite <- add_le_mono_l. destruct (mod_bound_pos p r); order.
 Qed.
 
 
@@ -371,7 +363,7 @@ Proof.
  intros.
  symmetry.
  apply mod_unique with (a/c+b); auto.
- apply mod_bound; auto.
+ apply mod_bound_pos; auto.
  rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
  now rewrite mul_comm.
 Qed.
@@ -404,8 +396,8 @@ Proof.
  apply div_unique with ((a mod b)*c).
  apply mul_nonneg_nonneg; order.
  split.
- apply mul_nonneg_nonneg; destruct (mod_bound a b); order.
- rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound a b); auto.
+ apply mul_nonneg_nonneg; destruct (mod_bound_pos a b); order.
+ rewrite <- mul_lt_mono_pos_r; auto. destruct (mod_bound_pos a b); auto.
  rewrite (div_mod a b) at 1 by order.
  rewrite mul_add_distr_r.
  rewrite add_cancel_r.
@@ -441,7 +433,7 @@ Qed.
 Theorem mod_mod: forall a n, 0<=a -> 0<n ->
  (a mod n) mod n == a mod n.
 Proof.
- intros. destruct (mod_bound a n); auto. now rewrite mod_small_iff.
+ intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff.
 Qed.
 
 Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -454,7 +446,7 @@ Proof.
  rewrite mul_add_distr_l, mul_assoc.
  intros. rewrite mod_add; auto.
  now rewrite mul_comm.
- apply mul_nonneg_nonneg; destruct (mod_bound a n); auto.
+ apply mul_nonneg_nonneg; destruct (mod_bound_pos a n); auto.
 Qed.
 
 Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -467,7 +459,7 @@ Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a * b) mod n == ((a mod n) * (b mod n)) mod n.
 Proof.
  intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. reflexivity.
- now destruct (mod_bound b n).
+ now destruct (mod_bound_pos b n).
 Qed.
 
 Lemma add_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -478,7 +470,7 @@ Proof.
  rewrite (div_mod a n) at 1 2 by order.
  rewrite <- add_assoc, add_comm, mul_comm.
  intros. rewrite mod_add; trivial. reflexivity.
- apply add_nonneg_nonneg; auto. destruct (mod_bound a n); auto.
+ apply add_nonneg_nonneg; auto. destruct (mod_bound_pos a n); auto.
 Qed.
 
 Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n ->
@@ -491,7 +483,7 @@ Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n ->
  (a+b) mod n == (a mod n + b mod n) mod n.
 Proof.
  intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. reflexivity.
- now destruct (mod_bound b n).
+ now destruct (mod_bound_pos b n).
 Qed.
 
 Lemma div_div : forall a b c, 0<=a -> 0<b -> 0<c ->
@@ -500,7 +492,7 @@ Proof.
  intros a b c Ha Hb Hc.
  apply div_unique with (b*((a/b) mod c) + a mod b); trivial.
  (* begin 0<= ... <b*c *)
- destruct (mod_bound (a/b) c), (mod_bound a b); auto using div_pos.
+ destruct (mod_bound_pos (a/b) c), (mod_bound_pos a b); auto using div_pos.
  split.
  apply add_nonneg_nonneg; auto.
  apply mul_nonneg_nonneg; order.
@@ -514,6 +506,18 @@ Proof.
  apply div_mod; order.
 Qed.
 
+Lemma mod_mul_r : forall a b c, 0<=a -> 0<b -> 0<c ->
+ a mod (b*c) == a mod b + b*((a/b) mod c).
+Proof.
+ intros a b c Ha Hb Hc.
+ apply add_cancel_l with (b*c*(a/(b*c))).
+ rewrite <- div_mod by (apply neq_mul_0; split; order).
+ rewrite <- div_div by trivial.
+ rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l.
+ rewrite <- div_mod by order.
+ apply div_mod; order.
+Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
@@ -538,5 +542,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 9dba3c3c..36aaa3e7 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-(*i $Id: NZDomain.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export NumPrelude NZAxioms.
 Require Import NZBase NZOrder NZAddOrder Plus Minus.
 
@@ -16,97 +14,36 @@ Require Import NZBase NZOrder NZAddOrder Plus Minus.
     translation from Peano numbers [nat] into NZ.
 *)
 
-(** First, a section about iterating a function. *)
-
-Section Iter.
-Variable A : Type.
-Fixpoint iter (f:A->A)(n:nat) : A -> A := fun a =>
-  match n with
-    | O => a
-    | S n => f (iter f n a)
-  end.
-Infix "^" := iter.
-
-Lemma iter_alt : forall f n m, (f^(Datatypes.S n)) m = (f^n) (f m).
-Proof.
-induction n; simpl; auto.
-intros; rewrite <- IHn; auto.
-Qed.
-
-Lemma iter_plus : forall f n n' m, (f^(n+n')) m = (f^n) ((f^n') m).
-Proof.
-induction n; simpl; auto.
-intros; rewrite IHn; auto.
-Qed.
+(** First, some complements about [nat_iter] *)
 
-Lemma iter_plus_bis : forall f n n' m, (f^(n+n')) m = (f^n') ((f^n) m).
-Proof.
-induction n; simpl; auto.
-intros. rewrite <- iter_alt, IHn; auto.
-Qed.
+Local Notation "f ^ n" := (nat_iter n f).
 
-Global Instance iter_wd (R:relation A) : Proper ((R==>R)==>eq==>R==>R) iter.
+Instance nat_iter_wd n {A} (R:relation A) :
+ Proper ((R==>R)==>R==>R) (nat_iter n).
 Proof.
-intros f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto.
+intros f f' Hf. induction n; simpl; red; auto.
 Qed.
 
-End Iter.
-Implicit Arguments iter [A].
-Local Infix "^" := iter.
-
-
 Module NZDomainProp (Import NZ:NZDomainSig').
+Include NZBaseProp NZ.
 
 (** * Relationship between points thanks to [succ] and [pred]. *)
 
-(** We prove that any points in NZ have a common descendant by [succ] *)
-
-Definition common_descendant n m := exists k, exists l, (S^k) n == (S^l) m.
-
-Instance common_descendant_wd : Proper (eq==>eq==>iff) common_descendant.
-Proof.
-unfold common_descendant. intros n n' Hn m m' Hm.
-setoid_rewrite Hn. setoid_rewrite Hm. auto with *.
-Qed.
-
-Instance common_descendant_equiv : Equivalence common_descendant.
-Proof.
-split; red.
-intros x. exists O; exists O. simpl; auto with *.
-intros x y (p & q & H); exists q; exists p; auto with *.
-intros x y z (p & q & Hpq) (r & s & Hrs).
-exists (r+p)%nat. exists (q+s)%nat.
-rewrite !iter_plus. rewrite Hpq, <-Hrs, <-iter_plus, <- iter_plus_bis.
-auto with *.
-Qed.
-
-Lemma common_descendant_with_0 : forall n, common_descendant n 0.
-Proof.
-apply bi_induction.
-intros n n' Hn. rewrite Hn; auto with *.
-reflexivity.
-split; intros (p & q & H).
-exists p; exists (Datatypes.S q). rewrite <- iter_alt; simpl.
- apply succ_wd; auto.
-exists (Datatypes.S p); exists q. rewrite iter_alt; auto.
-Qed.
-
-Lemma common_descendant_always : forall n m, common_descendant n m.
-Proof.
-intros. transitivity 0; [|symmetry]; apply common_descendant_with_0.
-Qed.
-
-(** Thanks to [succ] being injective, we can then deduce that for any two
-    points, one is an iterated successor of the other. *)
+(** For any two points, one is an iterated successor of the other. *)
 
-Lemma itersucc_or_itersucc : forall n m, exists k, n == (S^k) m \/ m == (S^k) n.
+Lemma itersucc_or_itersucc n m : exists k, n == (S^k) m \/ m == (S^k) n.
 Proof.
-intros n m. destruct (common_descendant_always n m) as (k & l & H).
-revert l H. induction k.
-simpl. intros; exists l; left; auto with *.
-intros. destruct l.
-simpl in *. exists (Datatypes.S k); right; auto with *.
-simpl in *. apply pred_wd in H; rewrite !pred_succ in H. eauto.
+nzinduct n m.
+exists 0%nat. now left.
+intros n. split; intros [k [L|R]].
+exists (Datatypes.S k). left. now apply succ_wd.
+destruct k as [|k].
+simpl in R. exists 1%nat. left. now apply succ_wd.
+rewrite nat_iter_succ_r in R. exists k. now right.
+destruct k as [|k]; simpl in L.
+exists 1%nat. now right.
+apply succ_inj in L. exists k. now left.
+exists (Datatypes.S k). right. now rewrite nat_iter_succ_r.
 Qed.
 
 (** Generalized version of [pred_succ] when iterating *)
@@ -116,7 +53,7 @@ Proof.
 induction k.
 simpl; auto with *.
 simpl; intros. apply pred_wd in H. rewrite pred_succ in H. apply IHk in H; auto.
-rewrite <- iter_alt in H; auto.
+rewrite <- nat_iter_succ_r in H; auto.
 Qed.
 
 (** From a given point, all others are iterated successors
@@ -307,7 +244,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 :
@@ -315,8 +252,8 @@ Theorem ofnat_S_gt_0 :
 Proof.
 unfold ofnat.
 intros n; induction n as [| n IH]; simpl in *.
-apply lt_0_1.
-apply lt_trans with 1. apply lt_0_1. now rewrite <- succ_lt_mono.
+apply lt_succ_diag_r.
+apply lt_trans with (S 0). apply lt_succ_diag_r. now rewrite <- succ_lt_mono.
 Qed.
 
 Theorem ofnat_S_neq_0 :
@@ -375,14 +312,14 @@ Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m.
 Proof.
  induction n; intros.
  apply add_0_l.
- rewrite ofnat_succ, add_succ_l. simpl; apply succ_wd; auto.
+ rewrite ofnat_succ, add_succ_l. simpl. now f_equiv.
 Qed.
 
 Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
 Proof.
  intros. rewrite ofnat_add_l.
  induction n; simpl. reflexivity.
- rewrite ofnat_succ. now apply succ_wd.
+ rewrite ofnat_succ. now f_equiv.
 Qed.
 
 Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -391,14 +328,14 @@ Proof.
  symmetry. apply mul_0_l.
  rewrite plus_comm.
  rewrite ofnat_succ, ofnat_add, mul_succ_l.
- now apply add_wd.
+ now f_equiv.
 Qed.
 
 Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
 Proof.
  induction m; simpl; intros.
  rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. now apply pred_wd.
+ rewrite ofnat_succ, sub_succ_r. now f_equiv.
 Qed.
 
 Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
@@ -409,7 +346,7 @@ Proof.
  intros.
  destruct n.
  inversion H.
- rewrite iter_alt.
+ rewrite nat_iter_succ_r.
  simpl.
  rewrite ofnat_succ, pred_succ; auto with arith.
 Qed.
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
new file mode 100644
index 00000000..f72023d9
--- /dev/null
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -0,0 +1,307 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Greatest Common Divisor *)
+
+Require Import NZAxioms NZMulOrder.
+
+(** Interface of a gcd function, then its specification on naturals *)
+
+Module Type Gcd (Import A : Typ).
+ Parameter Inline gcd : t -> t -> t.
+End Gcd.
+
+Module Type NZGcdSpec (A : NZOrdAxiomsSig')(B : Gcd A).
+ Import A B.
+ Definition divide n m := exists p, m == p*n.
+ Local Notation "( n | m )" := (divide n m) (at level 0).
+ Axiom gcd_divide_l : forall n m, (gcd n m | n).
+ Axiom gcd_divide_r : forall n m, (gcd n m | m).
+ Axiom gcd_greatest : forall n m p, (p | n) -> (p | m) -> (p | gcd n m).
+ Axiom gcd_nonneg : forall n m, 0 <= gcd n m.
+End NZGcdSpec.
+
+Module Type DivideNotation (A:NZOrdAxiomsSig')(B:Gcd A)(C:NZGcdSpec A B).
+ Import A B C.
+ Notation "( n | m )" := (divide n m) (at level 0).
+End DivideNotation.
+
+Module Type NZGcd (A : NZOrdAxiomsSig) := Gcd A <+ NZGcdSpec A.
+Module Type NZGcd' (A : NZOrdAxiomsSig) :=
+ Gcd A <+ NZGcdSpec A <+ DivideNotation A.
+
+(** Derived properties of gcd *)
+
+Module NZGcdProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZGcd' A)
+ (Import C : NZMulOrderProp A).
+
+(** Results concerning divisibility*)
+
+Instance divide_wd : Proper (eq==>eq==>iff) divide.
+Proof.
+ unfold divide. intros x x' Hx y y' Hy.
+ setoid_rewrite Hx. setoid_rewrite Hy. easy.
+Qed.
+
+Lemma divide_1_l : forall n, (1 | n).
+Proof.
+ intros n. exists n. now nzsimpl.
+Qed.
+
+Lemma divide_0_r : forall n, (n | 0).
+Proof.
+ intros n. exists 0. now nzsimpl.
+Qed.
+
+Hint Rewrite divide_1_l divide_0_r : nz.
+
+Lemma divide_0_l : forall n, (0 | n) -> n==0.
+Proof.
+ intros n (m,Hm). revert Hm. now nzsimpl.
+Qed.
+
+Lemma eq_mul_1_nonneg : forall n m,
+ 0<=n -> n*m == 1 -> n==1 /\ m==1.
+Proof.
+ intros n m Hn H.
+ le_elim Hn.
+ destruct (lt_ge_cases m 0) as [Hm|Hm].
+ generalize (mul_pos_neg n m Hn Hm). order'.
+ le_elim Hm.
+ apply le_succ_l in Hn. rewrite <- one_succ in Hn.
+ le_elim Hn.
+ generalize (lt_1_mul_pos n m Hn Hm). order.
+ rewrite <- Hn, mul_1_l in H. now split.
+ rewrite <- Hm, mul_0_r in H. order'.
+ rewrite <- Hn, mul_0_l in H. order'.
+Qed.
+
+Lemma eq_mul_1_nonneg' : forall n m,
+ 0<=m -> n*m == 1 -> n==1 /\ m==1.
+Proof.
+ intros n m Hm H. rewrite mul_comm in H.
+ now apply and_comm, eq_mul_1_nonneg.
+Qed.
+
+Lemma divide_1_r_nonneg : forall n, 0<=n -> (n | 1) -> n==1.
+Proof.
+ intros n Hn (m,Hm). symmetry in Hm.
+ now apply (eq_mul_1_nonneg' m n).
+Qed.
+
+Lemma divide_refl : forall n, (n | n).
+Proof.
+ intros n. exists 1. now nzsimpl.
+Qed.
+
+Lemma divide_trans : forall n m p, (n | m) -> (m | p) -> (n | p).
+Proof.
+ intros n m p (q,Hq) (r,Hr). exists (r*q).
+ now rewrite Hr, Hq, mul_assoc.
+Qed.
+
+Instance divide_reflexive : Reflexive divide := divide_refl.
+Instance divide_transitive : Transitive divide := divide_trans.
+
+(** Due to sign, no general antisymmetry result *)
+
+Lemma divide_antisym_nonneg : forall n m,
+ 0<=n -> 0<=m -> (n | m) -> (m | n) -> n == m.
+Proof.
+ intros n m Hn Hm (q,Hq) (r,Hr).
+ le_elim Hn.
+ destruct (lt_ge_cases q 0) as [Hq'|Hq'].
+ generalize (mul_neg_pos q n Hq' Hn). order.
+ rewrite Hq, mul_assoc in Hr. symmetry in Hr.
+ apply mul_id_l in Hr; [|order].
+ destruct (eq_mul_1_nonneg' r q) as [_ H]; trivial.
+ now rewrite H, mul_1_l in Hq.
+ rewrite <- Hn, mul_0_r in Hq. now rewrite <- Hn.
+Qed.
+
+Lemma mul_divide_mono_l : forall n m p, (n | m) -> (p * n | p * m).
+Proof.
+ intros n m p (q,Hq). exists q. now rewrite mul_shuffle3, Hq.
+Qed.
+
+Lemma mul_divide_mono_r : forall n m p, (n | m) -> (n * p | m * p).
+Proof.
+ intros n m p (q,Hq). exists q. now rewrite mul_assoc, Hq.
+Qed.
+
+Lemma mul_divide_cancel_l : forall n m p, p ~= 0 ->
+ ((p * n | p * m) <-> (n | m)).
+Proof.
+ intros n m p Hp. split.
+ intros (q,Hq). exists q. now rewrite mul_shuffle3, mul_cancel_l in Hq.
+ apply mul_divide_mono_l.
+Qed.
+
+Lemma mul_divide_cancel_r : forall n m p, p ~= 0 ->
+ ((n * p | m * p) <-> (n | m)).
+Proof.
+ intros. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l.
+Qed.
+
+Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p).
+Proof.
+ intros n m p (q,Hq) (r,Hr). exists (q+r).
+ now rewrite mul_add_distr_r, Hq, Hr.
+Qed.
+
+Lemma divide_mul_l : forall n m p, (n | m) -> (n | m * p).
+Proof.
+ intros n m p (q,Hq). exists (q*p). now rewrite mul_shuffle0, Hq.
+Qed.
+
+Lemma divide_mul_r : forall n m p, (n | p) -> (n | m * p).
+Proof.
+ intros n m p. rewrite mul_comm. apply divide_mul_l.
+Qed.
+
+Lemma divide_factor_l : forall n m, (n | n * m).
+Proof.
+ intros. apply divide_mul_l, divide_refl.
+Qed.
+
+Lemma divide_factor_r : forall n m, (n | m * n).
+Proof.
+ intros. apply divide_mul_r, divide_refl.
+Qed.
+
+Lemma divide_pos_le : forall n m, 0 < m -> (n | m) -> n <= m.
+Proof.
+ intros n m Hm (q,Hq).
+ destruct (le_gt_cases n 0) as [Hn|Hn]. order.
+ rewrite Hq.
+ destruct (lt_ge_cases q 0) as [Hq'|Hq'].
+ generalize (mul_neg_pos q n Hq' Hn). order.
+ le_elim Hq'.
+ rewrite <- (mul_1_l n) at 1. apply mul_le_mono_pos_r; trivial.
+ now rewrite one_succ, le_succ_l.
+ rewrite <- Hq', mul_0_l in Hq. order.
+Qed.
+
+(** Basic properties of gcd *)
+
+Lemma gcd_unique : forall n m p,
+ 0<=p -> (p|n) -> (p|m) ->
+ (forall q, (q|n) -> (q|m) -> (q|p)) ->
+ gcd n m == p.
+Proof.
+ intros n m p Hp Hn Hm H.
+ apply divide_antisym_nonneg; trivial. apply gcd_nonneg.
+ apply H. apply gcd_divide_l. apply gcd_divide_r.
+ now apply gcd_greatest.
+Qed.
+
+Instance gcd_wd : Proper (eq==>eq==>eq) gcd.
+Proof.
+ intros x x' Hx y y' Hy.
+ apply gcd_unique.
+ apply gcd_nonneg.
+ rewrite Hx. apply gcd_divide_l.
+ rewrite Hy. apply gcd_divide_r.
+ intro. rewrite Hx, Hy. apply gcd_greatest.
+Qed.
+
+Lemma gcd_divide_iff : forall n m p,
+  (p | gcd n m) <-> (p | n) /\ (p | m).
+Proof.
+ intros. split. split.
+ transitivity (gcd n m); trivial using gcd_divide_l.
+ transitivity (gcd n m); trivial using gcd_divide_r.
+ intros (H,H'). now apply gcd_greatest.
+Qed.
+
+Lemma gcd_unique_alt : forall n m p, 0<=p ->
+ (forall q, (q|p) <-> (q|n) /\ (q|m)) ->
+ gcd n m == p.
+Proof.
+ intros n m p Hp H.
+ apply gcd_unique; trivial.
+ apply H. apply divide_refl.
+ apply H. apply divide_refl.
+ intros. apply H. now split.
+Qed.
+
+Lemma gcd_comm : forall n m, gcd n m == gcd m n.
+Proof.
+ intros. apply gcd_unique_alt; try apply gcd_nonneg.
+ intros. rewrite and_comm. apply gcd_divide_iff.
+Qed.
+
+Lemma gcd_assoc : forall n m p, gcd n (gcd m p) == gcd (gcd n m) p.
+Proof.
+ intros. apply gcd_unique_alt; try apply gcd_nonneg.
+ intros. now rewrite !gcd_divide_iff, and_assoc.
+Qed.
+
+Lemma gcd_0_l_nonneg : forall n, 0<=n -> gcd 0 n == n.
+Proof.
+ intros. apply gcd_unique; trivial.
+ apply divide_0_r.
+ apply divide_refl.
+Qed.
+
+Lemma gcd_0_r_nonneg : forall n, 0<=n -> gcd n 0 == n.
+Proof.
+ intros. now rewrite gcd_comm, gcd_0_l_nonneg.
+Qed.
+
+Lemma gcd_1_l : forall n, gcd 1 n == 1.
+Proof.
+ intros. apply gcd_unique; trivial using divide_1_l, le_0_1.
+Qed.
+
+Lemma gcd_1_r : forall n, gcd n 1 == 1.
+Proof.
+ intros. now rewrite gcd_comm, gcd_1_l.
+Qed.
+
+Lemma gcd_diag_nonneg : forall n, 0<=n -> gcd n n == n.
+Proof.
+ intros. apply gcd_unique; trivial using divide_refl.
+Qed.
+
+Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0.
+Proof.
+ intros.
+ generalize (gcd_divide_l n m). rewrite H. apply divide_0_l.
+Qed.
+
+Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0.
+Proof.
+ intros. apply gcd_eq_0_l with n. now rewrite gcd_comm.
+Qed.
+
+Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0.
+Proof.
+ intros. split. split.
+ now apply gcd_eq_0_l with m.
+ now apply gcd_eq_0_r with n.
+ intros (EQ,EQ'). rewrite EQ, EQ'. now apply gcd_0_r_nonneg.
+Qed.
+
+Lemma gcd_mul_diag_l : forall n m, 0<=n -> gcd n (n*m) == n.
+Proof.
+ intros n m Hn. apply gcd_unique_alt; trivial.
+ intros q. split. split; trivial. now apply divide_mul_l.
+ now destruct 1.
+Qed.
+
+Lemma divide_gcd_iff : forall n m, 0<=n -> ((n|m) <-> gcd n m == n).
+Proof.
+ intros n m Hn. split. intros (q,Hq). rewrite Hq.
+ rewrite mul_comm. now apply gcd_mul_diag_l.
+ intros EQ. rewrite <- EQ. apply gcd_divide_r.
+Qed.
+
+End NZGcdProp.
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
new file mode 100644
index 00000000..a5aa6d8a
--- /dev/null
+++ b/theories/Numbers/NatInt/NZLog.v
@@ -0,0 +1,889 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Base-2 Logarithm *)
+
+Require Import NZAxioms NZMulOrder NZPow.
+
+(** Interface of a log2 function, then its specification on naturals *)
+
+Module Type Log2 (Import A : Typ).
+ Parameter Inline log2 : t -> t.
+End Log2.
+
+Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A).
+ Import A B C.
+ Axiom log2_spec : forall a, 0<a -> 2^(log2 a) <= a < 2^(S (log2 a)).
+ Axiom log2_nonpos : forall a, a<=0 -> log2 a == 0.
+End NZLog2Spec.
+
+Module Type NZLog2 (A : NZOrdAxiomsSig)(B : Pow A) := Log2 A <+ NZLog2Spec A B.
+
+(** Derived properties of logarithm *)
+
+Module Type NZLog2Prop
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZPow' A)
+ (Import C : NZLog2 A B)
+ (Import D : NZMulOrderProp A)
+ (Import E : NZPowProp A B D).
+
+(** log2 is always non-negative *)
+
+Lemma log2_nonneg : forall a, 0 <= log2 a.
+Proof.
+ intros a. destruct (le_gt_cases a 0) as [Ha|Ha].
+ now rewrite log2_nonpos.
+ destruct (log2_spec a Ha) as (_,LT).
+ apply lt_succ_r, (pow_gt_1 2). order'.
+ rewrite <- le_succ_l, <- one_succ in Ha. order.
+Qed.
+
+(** A tactic for proving positivity and non-negativity *)
+
+Ltac order_pos :=
+((apply add_pos_pos || apply add_nonneg_nonneg ||
+  apply mul_pos_pos || apply mul_nonneg_nonneg ||
+  apply pow_nonneg || apply pow_pos_nonneg ||
+  apply log2_nonneg || apply (le_le_succ_r 0));
+ order_pos) (* in case of success of an apply, we recurse *)
+|| order'.  (* otherwise *)
+
+(** The spec of log2 indeed determines it *)
+
+Lemma log2_unique : forall a b, 0<=b -> 2^b<=a<2^(S b) -> log2 a == b.
+Proof.
+ intros a b Hb (LEb,LTb).
+ assert (Ha : 0 < a).
+  apply lt_le_trans with (2^b); trivial.
+  apply pow_pos_nonneg; order'.
+ assert (Hc := log2_nonneg a).
+ destruct (log2_spec a Ha) as (LEc,LTc).
+ assert (log2 a <= b).
+  apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
+  now apply le_le_succ_r.
+ assert (b <= log2 a).
+  apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
+  now apply le_le_succ_r.
+ order.
+Qed.
+
+(** Hence log2 is a morphism. *)
+
+Instance log2_wd : Proper (eq==>eq) log2.
+Proof.
+ intros x x' Hx.
+ destruct (le_gt_cases x 0).
+ rewrite 2 log2_nonpos; trivial. reflexivity. now rewrite <- Hx.
+ apply log2_unique. apply log2_nonneg.
+ rewrite Hx in *. now apply log2_spec.
+Qed.
+
+(** An alternate specification *)
+
+Lemma log2_spec_alt : forall a, 0<a -> exists r,
+ a == 2^(log2 a) + r /\ 0 <= r < 2^(log2 a).
+Proof.
+ intros a Ha.
+ destruct (log2_spec _ Ha) as (LE,LT).
+ destruct (le_exists_sub _ _ LE) as (r & Hr & Hr').
+ exists r.
+ split. now rewrite add_comm.
+ split. trivial.
+ apply (add_lt_mono_r _ _ (2^log2 a)).
+ rewrite <- Hr. generalize LT.
+ rewrite pow_succ_r by order_pos.
+ rewrite two_succ at 1. now nzsimpl.
+Qed.
+
+Lemma log2_unique' : forall a b c, 0<=b -> 0<=c<2^b ->
+ a == 2^b + c -> log2 a == b.
+Proof.
+ intros a b c Hb (Hc,H) EQ.
+ apply log2_unique. trivial.
+ rewrite EQ.
+ split.
+ rewrite <- add_0_r at 1. now apply add_le_mono_l.
+ rewrite pow_succ_r by order.
+ rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l.
+Qed.
+
+(** log2 is exact on powers of 2 *)
+
+Lemma log2_pow2 : forall a, 0<=a -> log2 (2^a) == a.
+Proof.
+ intros a Ha.
+ apply log2_unique' with 0; trivial.
+ split; order_pos. now nzsimpl.
+Qed.
+
+(** log2 and predecessors of powers of 2 *)
+
+Lemma log2_pred_pow2 : forall a, 0<a -> log2 (P (2^a)) == P a.
+Proof.
+ intros a Ha.
+ assert (Ha' : S (P a) == a) by (now rewrite lt_succ_pred with 0).
+ apply log2_unique.
+ apply lt_succ_r; order.
+ rewrite <-le_succ_l, <-lt_succ_r, Ha'.
+ rewrite lt_succ_pred with 0.
+ split; try easy. apply pow_lt_mono_r_iff; try order'.
+  rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r.
+ apply pow_pos_nonneg; order'.
+Qed.
+
+(** log2 and basic constants *)
+
+Lemma log2_1 : log2 1 == 0.
+Proof.
+ rewrite <- (pow_0_r 2). now apply log2_pow2.
+Qed.
+
+Lemma log2_2 : log2 2 == 1.
+Proof.
+ rewrite <- (pow_1_r 2). apply log2_pow2; order'.
+Qed.
+
+(** log2 n is strictly positive for 1<n *)
+
+Lemma log2_pos : forall a, 1<a -> 0 < log2 a.
+Proof.
+ intros a Ha.
+ assert (Ha' : 0 < a) by order'.
+ assert (H := log2_nonneg a). le_elim H; trivial.
+ generalize (log2_spec a Ha'). rewrite <- H in *. nzsimpl; try order.
+ intros (_,H'). rewrite two_succ in H'. apply lt_succ_r in H'; order.
+Qed.
+
+(** Said otherwise, log2 is null only below 1 *)
+
+Lemma log2_null : forall a, log2 a == 0 <-> a <= 1.
+Proof.
+ intros a. split; intros H.
+ destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
+ generalize (log2_pos a Ha); order.
+ le_elim H.
+ apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ.
+ rewrite H. apply log2_1.
+Qed.
+
+(** log2 is a monotone function (but not a strict one) *)
+
+Lemma log2_le_mono : forall a b, a<=b -> log2 a <= log2 b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases a 0) as [Ha|Ha].
+ rewrite log2_nonpos; order_pos.
+ assert (Hb : 0 < b) by order.
+ destruct (log2_spec a Ha) as (LEa,_).
+ destruct (log2_spec b Hb) as (_,LTb).
+ apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos.
+Qed.
+
+(** No reverse result for <=, consider for instance log2 3 <= log2 2 *)
+
+Lemma log2_lt_cancel : forall a b, log2 a < log2 b -> a < b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases b 0) as [Hb|Hb].
+  rewrite (log2_nonpos b) in H; trivial.
+  generalize (log2_nonneg a); order.
+ destruct (le_gt_cases a 0) as [Ha|Ha]. order.
+ destruct (log2_spec a Ha) as (_,LTa).
+ destruct (log2_spec b Hb) as (LEb,_).
+ apply le_succ_l in H.
+ apply (pow_le_mono_r_iff 2) in H; order_pos.
+Qed.
+
+(** When left side is a power of 2, we have an equivalence for <= *)
+
+Lemma log2_le_pow2 : forall a b, 0<a -> (2^b<=a <-> b <= log2 a).
+Proof.
+ intros a b Ha.
+ split; intros H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ generalize (log2_nonneg a); order.
+ rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono.
+ transitivity (2^(log2 a)).
+ apply pow_le_mono_r; order'.
+ now destruct (log2_spec a Ha).
+Qed.
+
+(** When right side is a square, we have an equivalence for < *)
+
+Lemma log2_lt_pow2 : forall a b, 0<a -> (a<2^b <-> log2 a < b).
+Proof.
+ intros a b Ha.
+ split; intros H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite pow_neg_r in H; order.
+ apply (pow_lt_mono_r_iff 2); try order_pos.
+ apply le_lt_trans with a; trivial.
+ now destruct (log2_spec a Ha).
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ generalize (log2_nonneg a); order.
+ apply log2_lt_cancel; try order.
+ now rewrite log2_pow2.
+Qed.
+
+(** Comparing log2 and identity *)
+
+Lemma log2_lt_lin : forall a, 0<a -> log2 a < a.
+Proof.
+ intros a Ha.
+ apply (pow_lt_mono_r_iff 2); try order_pos.
+ apply le_lt_trans with a.
+ now destruct (log2_spec a Ha).
+ apply pow_gt_lin_r; order'.
+Qed.
+
+Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a.
+Proof.
+ intros a Ha.
+ le_elim Ha.
+ now apply lt_le_incl, log2_lt_lin.
+ rewrite <- Ha, log2_nonpos; order.
+Qed.
+
+(** Log2 and multiplication. *)
+
+(** Due to rounding error, we don't have the usual
+    [log2 (a*b) = log2 a + log2 b] but we may be off by 1 at most *)
+
+Lemma log2_mul_below : forall a b, 0<a -> 0<b ->
+ log2 a + log2 b <= log2 (a*b).
+Proof.
+ intros a b Ha Hb.
+ apply log2_le_pow2; try order_pos.
+ rewrite pow_add_r by order_pos.
+ apply mul_le_mono_nonneg; try apply log2_spec; order_pos.
+Qed.
+
+Lemma log2_mul_above : forall a b, 0<=a -> 0<=b ->
+ log2 (a*b) <= log2 a + log2 b + 1.
+Proof.
+ intros a b Ha Hb.
+ le_elim Ha.
+ le_elim Hb.
+ apply lt_succ_r.
+ rewrite add_1_r, <- add_succ_r, <- add_succ_l.
+ apply log2_lt_pow2; try order_pos.
+ rewrite pow_add_r by order_pos.
+ apply mul_lt_mono_nonneg; try order; now apply log2_spec.
+ rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos.
+ rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos.
+Qed.
+
+(** And we can't find better approximations in general.
+    - The lower bound is exact for powers of 2.
+    - Concerning the upper bound, for any c>1, take a=b=2^c-1,
+      then log2 (a*b) = c+c -1 while (log2 a) = (log2 b) = c-1
+*)
+
+(** At least, we get back the usual equation when we multiply by 2 (or 2^k) *)
+
+Lemma log2_mul_pow2 : forall a b, 0<a -> 0<=b -> log2 (a*2^b) == b + log2 a.
+Proof.
+ intros a b Ha Hb.
+ apply log2_unique; try order_pos. split.
+ rewrite pow_add_r, mul_comm; try order_pos.
+ apply mul_le_mono_nonneg_r. order_pos. now apply log2_spec.
+ rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos.
+ apply mul_lt_mono_pos_l. order_pos. now apply log2_spec.
+Qed.
+
+Lemma log2_double : forall a, 0<a -> log2 (2*a) == S (log2 a).
+Proof.
+ intros a Ha. generalize (log2_mul_pow2 a 1 Ha le_0_1). now nzsimpl'.
+Qed.
+
+(** Two numbers with same log2 cannot be far away. *)
+
+Lemma log2_same : forall a b, 0<a -> 0<b -> log2 a == log2 b -> a < 2*b.
+Proof.
+ intros a b Ha Hb H.
+ apply log2_lt_cancel. rewrite log2_double, H by trivial.
+ apply lt_succ_diag_r.
+Qed.
+
+(** Log2 and successor :
+    - the log2 function climbs by at most 1 at a time
+    - otherwise it stays at the same value
+    - the +1 steps occur for powers of two
+*)
+
+Lemma log2_succ_le : forall a, log2 (S a) <= S (log2 a).
+Proof.
+ intros a.
+ destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]].
+ apply (pow_le_mono_r_iff 2); try order_pos.
+ transitivity (S a).
+ apply log2_spec.
+ apply lt_succ_r; order.
+ now apply le_succ_l, log2_spec.
+ rewrite <- EQ, <- one_succ, log2_1; order_pos.
+ rewrite 2 log2_nonpos. order_pos. order'. now rewrite le_succ_l.
+Qed.
+
+Lemma log2_succ_or : forall a,
+ log2 (S a) == S (log2 a) \/ log2 (S a) == log2 a.
+Proof.
+ intros.
+ destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H].
+ right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order.
+ left. apply le_succ_l in H. generalize (log2_succ_le a); order.
+Qed.
+
+Lemma log2_eq_succ_is_pow2 : forall a,
+ log2 (S a) == S (log2 a) -> exists b, S a == 2^b.
+Proof.
+ intros a H.
+ destruct (le_gt_cases a 0) as [Ha|Ha].
+ rewrite 2 (proj2 (log2_null _)) in H. generalize (lt_succ_diag_r 0); order.
+ order'. apply le_succ_l. order'.
+ assert (Ha' : 0 < S a) by (apply lt_succ_r; order).
+ exists (log2 (S a)).
+ generalize (proj1 (log2_spec (S a) Ha')) (proj2 (log2_spec a Ha)).
+ rewrite <- le_succ_l, <- H. order.
+Qed.
+
+Lemma log2_eq_succ_iff_pow2 : forall a, 0<a ->
+ (log2 (S a) == S (log2 a) <-> exists b, S a == 2^b).
+Proof.
+ intros a Ha.
+ split. apply log2_eq_succ_is_pow2.
+ intros (b,Hb).
+ assert (Hb' : 0 < b).
+  apply (pow_gt_1 2); try order'; now rewrite <- Hb, one_succ, <- succ_lt_mono.
+ rewrite Hb, log2_pow2; try order'.
+ setoid_replace a with (P (2^b)). rewrite log2_pred_pow2; trivial.
+ symmetry; now apply lt_succ_pred with 0.
+ apply succ_inj. rewrite Hb. symmetry. apply lt_succ_pred with 0.
+  rewrite <- Hb, lt_succ_r; order.
+Qed.
+
+Lemma log2_succ_double : forall a, 0<a -> log2 (2*a+1) == S (log2 a).
+Proof.
+ intros a Ha.
+ rewrite add_1_r.
+ destruct (log2_succ_or (2*a)) as [H|H]; [exfalso|now rewrite H, log2_double].
+ apply log2_eq_succ_is_pow2 in H. destruct H as (b,H).
+ destruct (lt_trichotomy b 0) as [LT|[EQ|LT]].
+ rewrite pow_neg_r in H; trivial.
+ apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'.
+ rewrite <- one_succ in Ha. order'.
+ rewrite EQ, pow_0_r in H.
+ apply (mul_pos_pos 2), succ_lt_mono in Ha; try order'.
+ rewrite <- one_succ in Ha. order'.
+ assert (EQ:=lt_succ_pred 0 b LT).
+ rewrite <- EQ, pow_succ_r in H; [|now rewrite <- lt_succ_r, EQ].
+ destruct (lt_ge_cases a (2^(P b))) as [LT'|LE'].
+ generalize (mul_2_mono_l _ _ LT'). rewrite add_1_l. order.
+ rewrite (mul_le_mono_pos_l _ _ 2) in LE'; try order'.
+ rewrite <- H in LE'. apply le_succ_l in LE'. order.
+Qed.
+
+(** Log2 and addition *)
+
+Lemma log2_add_le : forall a b, a~=1 -> b~=1 -> log2 (a+b) <= log2 a + log2 b.
+Proof.
+ intros a b Ha Hb.
+ destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|].
+ rewrite one_succ, lt_succ_r in Ha'.
+ rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono.
+ rewrite <- (add_0_l b) at 2. now apply add_le_mono.
+ destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|].
+ rewrite one_succ, lt_succ_r in Hb'.
+ rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono.
+ rewrite <- (add_0_r a) at 2. now apply add_le_mono.
+ clear Ha Hb.
+ apply lt_succ_r.
+ apply log2_lt_pow2; try order_pos.
+ rewrite pow_succ_r by order_pos.
+ rewrite two_succ, one_succ at 1. nzsimpl.
+ apply add_lt_mono.
+ apply lt_le_trans with (2^(S (log2 a))). apply log2_spec; order'.
+ apply pow_le_mono_r. order'. rewrite <- add_1_r. apply add_le_mono_l.
+  rewrite one_succ; now apply le_succ_l, log2_pos.
+ apply lt_le_trans with (2^(S (log2 b))). apply log2_spec; order'.
+ apply pow_le_mono_r. order'. rewrite <- add_1_l. apply add_le_mono_r.
+  rewrite one_succ; now apply le_succ_l, log2_pos.
+Qed.
+
+(** The sum of two log2 is less than twice the log2 of the sum.
+    The large inequality is obvious thanks to monotonicity.
+    The strict one requires some more work. This is almost
+    a convexity inequality for points [2a], [2b] and their middle [a+b] :
+    ideally, we would have [2*log(a+b) >= log(2a)+log(2b) = 2+log a+log b].
+    Here, we cannot do better: consider for instance a=2 b=4, then 1+2<2*2
+*)
+
+Lemma add_log2_lt : forall a b, 0<a -> 0<b ->
+ log2 a + log2 b < 2 * log2 (a+b).
+Proof.
+ intros a b Ha Hb. nzsimpl'.
+ assert (H : log2 a <= log2 (a+b)).
+  apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order.
+ assert (H' : log2 b <= log2 (a+b)).
+  apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
+ le_elim H.
+ apply lt_le_trans with (log2 (a+b) + log2 b).
+  now apply add_lt_mono_r. now apply add_le_mono_l.
+ rewrite <- H at 1. apply add_lt_mono_l.
+ le_elim H'; trivial.
+ symmetry in H. apply log2_same in H; try order_pos.
+ symmetry in H'. apply log2_same in H'; try order_pos.
+ revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order.
+Qed.
+
+End NZLog2Prop.
+
+Module NZLog2UpProp
+ (Import A : NZDecOrdAxiomsSig')
+ (Import B : NZPow' A)
+ (Import C : NZLog2 A B)
+ (Import D : NZMulOrderProp A)
+ (Import E : NZPowProp A B D)
+ (Import F : NZLog2Prop A B C D E).
+
+(** * [log2_up] : a binary logarithm that rounds up instead of down *)
+
+(** For once, we define instead of axiomatizing, thanks to log2 *)
+
+Definition log2_up a :=
+ match compare 1 a with
+  | Lt => S (log2 (P a))
+  | _ => 0
+ end.
+
+Lemma log2_up_eqn0 : forall a, a<=1 -> log2_up a == 0.
+Proof.
+ intros a Ha. unfold log2_up. case compare_spec; try order.
+Qed.
+
+Lemma log2_up_eqn : forall a, 1<a -> log2_up a == S (log2 (P a)).
+Proof.
+ intros a Ha. unfold log2_up. case compare_spec; try order.
+Qed.
+
+Lemma log2_up_spec : forall a, 1<a ->
+ 2^(P (log2_up a)) < a <= 2^(log2_up a).
+Proof.
+ intros a Ha.
+ rewrite log2_up_eqn; trivial.
+ rewrite pred_succ.
+ rewrite <- (lt_succ_pred 1 a Ha) at 2 3.
+ rewrite lt_succ_r, le_succ_l.
+ apply log2_spec.
+ apply succ_lt_mono. now rewrite (lt_succ_pred 1 a Ha), <- one_succ.
+Qed.
+
+Lemma log2_up_nonpos : forall a, a<=0 -> log2_up a == 0.
+Proof.
+ intros. apply log2_up_eqn0. order'.
+Qed.
+
+Instance log2_up_wd : Proper (eq==>eq) log2_up.
+Proof.
+ assert (Proper (eq==>eq==>Logic.eq) compare).
+  repeat red; intros; do 2 case compare_spec; trivial; order.
+ intros a a' Ha. unfold log2_up. rewrite Ha at 1.
+ case compare; now rewrite ?Ha.
+Qed.
+
+(** [log2_up] is always non-negative *)
+
+Lemma log2_up_nonneg : forall a, 0 <= log2_up a.
+Proof.
+ intros a. unfold log2_up. case compare_spec; try order.
+ intros. apply le_le_succ_r, log2_nonneg.
+Qed.
+
+(** The spec of [log2_up] indeed determines it *)
+
+Lemma log2_up_unique : forall a b, 0<b -> 2^(P b)<a<=2^b -> log2_up a == b.
+Proof.
+ intros a b Hb (LEb,LTb).
+ assert (Ha : 1 < a).
+  apply le_lt_trans with (2^(P b)); trivial.
+  rewrite one_succ. apply le_succ_l.
+  apply pow_pos_nonneg. order'. apply lt_succ_r.
+  now rewrite (lt_succ_pred 0 b Hb).
+ assert (Hc := log2_up_nonneg a).
+ destruct (log2_up_spec a Ha) as (LTc,LEc).
+ assert (b <= log2_up a).
+  apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb).
+  rewrite <- succ_lt_mono.
+  apply (pow_lt_mono_r_iff 2); try order'.
+ assert (Hc' : 0 < log2_up a) by order.
+ assert (log2_up a <= b).
+  apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc').
+  rewrite <- succ_lt_mono.
+  apply (pow_lt_mono_r_iff 2); try order'.
+ order.
+Qed.
+
+(** [log2_up] is exact on powers of 2 *)
+
+Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a.
+Proof.
+ intros a Ha.
+ le_elim Ha.
+ apply log2_up_unique; trivial.
+ split; try order.
+ apply pow_lt_mono_r; try order'.
+ rewrite <- (lt_succ_pred 0 a Ha) at 2.
+ now apply lt_succ_r.
+ now rewrite <- Ha, pow_0_r, log2_up_eqn0.
+Qed.
+
+(** [log2_up] and successors of powers of 2 *)
+
+Lemma log2_up_succ_pow2 : forall a, 0<=a -> log2_up (S (2^a)) == S a.
+Proof.
+ intros a Ha.
+ rewrite log2_up_eqn, pred_succ, log2_pow2; try easy.
+ rewrite one_succ, <- succ_lt_mono. apply pow_pos_nonneg; order'.
+Qed.
+
+(** Basic constants *)
+
+Lemma log2_up_1 : log2_up 1 == 0.
+Proof.
+ now apply log2_up_eqn0.
+Qed.
+
+Lemma log2_up_2 : log2_up 2 == 1.
+Proof.
+ rewrite <- (pow_1_r 2). apply log2_up_pow2; order'.
+Qed.
+
+(** Links between log2 and [log2_up] *)
+
+Lemma le_log2_log2_up : forall a, log2 a <= log2_up a.
+Proof.
+ intros a. unfold log2_up. case compare_spec; intros H.
+ rewrite <- H, log2_1. order.
+ rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le.
+ rewrite log2_nonpos. order. now rewrite <-lt_succ_r, <-one_succ.
+Qed.
+
+Lemma le_log2_up_succ_log2 : forall a, log2_up a <= S (log2 a).
+Proof.
+ intros a. unfold log2_up. case compare_spec; intros H; try order_pos.
+ rewrite <- succ_le_mono. apply log2_le_mono.
+ rewrite <- (lt_succ_pred 1 a H) at 2. apply le_succ_diag_r.
+Qed.
+
+Lemma log2_log2_up_spec : forall a, 0<a ->
+ 2^log2 a <= a <= 2^log2_up a.
+Proof.
+ intros a H. split.
+ now apply log2_spec.
+ rewrite <-le_succ_l, <-one_succ in H. le_elim H.
+ now apply log2_up_spec.
+ now rewrite <-H, log2_up_1, pow_0_r.
+Qed.
+
+Lemma log2_log2_up_exact :
+ forall a, 0<a -> (log2 a == log2_up a <-> exists b, a == 2^b).
+Proof.
+ intros a Ha.
+ split. intros. exists (log2 a).
+  generalize (log2_log2_up_spec a Ha). rewrite <-H.
+  destruct 1; order.
+ intros (b,Hb). rewrite Hb.
+ destruct (le_gt_cases 0 b).
+ now rewrite log2_pow2, log2_up_pow2.
+ rewrite pow_neg_r; trivial. now rewrite log2_nonpos, log2_up_nonpos.
+Qed.
+
+(** [log2_up] n is strictly positive for 1<n *)
+
+Lemma log2_up_pos : forall a, 1<a -> 0 < log2_up a.
+Proof.
+ intros. rewrite log2_up_eqn; trivial. apply lt_succ_r; order_pos.
+Qed.
+
+(** Said otherwise, [log2_up] is null only below 1 *)
+
+Lemma log2_up_null : forall a, log2_up a == 0 <-> a <= 1.
+Proof.
+ intros a. split; intros H.
+ destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
+ generalize (log2_up_pos a Ha); order.
+ now apply log2_up_eqn0.
+Qed.
+
+(** [log2_up] is a monotone function (but not a strict one) *)
+
+Lemma log2_up_le_mono : forall a b, a<=b -> log2_up a <= log2_up b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases a 1) as [Ha|Ha].
+ rewrite log2_up_eqn0; trivial. apply log2_up_nonneg.
+ rewrite 2 log2_up_eqn; try order.
+ rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono.
+ rewrite 2 lt_succ_pred with 1; order.
+Qed.
+
+(** No reverse result for <=, consider for instance log2_up 4 <= log2_up 3 *)
+
+Lemma log2_up_lt_cancel : forall a b, log2_up a < log2_up b -> a < b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases b 1) as [Hb|Hb].
+  rewrite (log2_up_eqn0 b) in H; trivial.
+  generalize (log2_up_nonneg a); order.
+ destruct (le_gt_cases a 1) as [Ha|Ha]. order.
+ rewrite 2 log2_up_eqn in H; try order.
+ rewrite <- succ_lt_mono in H. apply log2_lt_cancel, succ_lt_mono in H.
+ rewrite 2 lt_succ_pred with 1 in H; order.
+Qed.
+
+(** When left side is a power of 2, we have an equivalence for < *)
+
+Lemma log2_up_lt_pow2 : forall a b, 0<a -> (2^b<a <-> b < log2_up a).
+Proof.
+ intros a b Ha.
+ split; intros H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ generalize (log2_up_nonneg a); order.
+ apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg.
+ apply lt_le_trans with a; trivial.
+ apply (log2_up_spec a).
+ apply le_lt_trans with (2^b); trivial.
+ rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ now rewrite pow_neg_r.
+ rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel.
+Qed.
+
+(** When right side is a square, we have an equivalence for <= *)
+
+Lemma log2_up_le_pow2 : forall a b, 0<a -> (a<=2^b <-> log2_up a <= b).
+Proof.
+ intros a b Ha.
+ split; intros H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite pow_neg_r in H; order.
+ rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono.
+ transitivity (2^(log2_up a)).
+ now apply log2_log2_up_spec.
+ apply pow_le_mono_r; order'.
+Qed.
+
+(** Comparing [log2_up] and identity *)
+
+Lemma log2_up_lt_lin : forall a, 0<a -> log2_up a < a.
+Proof.
+ intros a Ha.
+ assert (H : S (P a) == a) by (now apply lt_succ_pred with 0).
+ rewrite <- H at 2. apply lt_succ_r. apply log2_up_le_pow2; trivial.
+ rewrite <- H at 1. apply le_succ_l.
+ apply pow_gt_lin_r. order'. apply lt_succ_r; order.
+Qed.
+
+Lemma log2_up_le_lin : forall a, 0<=a -> log2_up a <= a.
+Proof.
+ intros a Ha.
+ le_elim Ha.
+ now apply lt_le_incl, log2_up_lt_lin.
+ rewrite <- Ha, log2_up_nonpos; order.
+Qed.
+
+(** [log2_up] and multiplication. *)
+
+(** Due to rounding error, we don't have the usual
+    [log2_up (a*b) = log2_up a + log2_up b] but we may be off by 1 at most *)
+
+Lemma log2_up_mul_above : forall a b, 0<=a -> 0<=b ->
+  log2_up (a*b) <= log2_up a + log2_up b.
+Proof.
+ intros a b Ha Hb.
+ assert (Ha':=log2_up_nonneg a).
+ assert (Hb':=log2_up_nonneg b).
+ le_elim Ha.
+ le_elim Hb.
+ apply log2_up_le_pow2; try order_pos.
+ rewrite pow_add_r; trivial.
+ apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'.
+ rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos.
+ rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos.
+Qed.
+
+Lemma log2_up_mul_below : forall a b, 0<a -> 0<b ->
+ log2_up a + log2_up b <= S (log2_up (a*b)).
+Proof.
+ intros a b Ha Hb.
+ rewrite <-le_succ_l, <-one_succ in Ha. le_elim Ha.
+ rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb.
+ assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial).
+ assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial).
+ rewrite <- (lt_succ_pred 0 (log2_up a)); trivial.
+ rewrite <- (lt_succ_pred 0 (log2_up b)); trivial.
+ nzsimpl. rewrite <- succ_le_mono, le_succ_l.
+ apply (pow_lt_mono_r_iff 2). order'. apply log2_up_nonneg.
+ rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial).
+ apply lt_le_trans with (a*b).
+ apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec.
+ apply log2_up_spec.
+ setoid_replace 1 with (1*1) by now nzsimpl.
+ apply mul_lt_mono_nonneg; order'.
+ rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r.
+ rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r.
+Qed.
+
+(** And we can't find better approximations in general.
+    - The upper bound is exact for powers of 2.
+    - Concerning the lower bound, for any c>1, take a=b=2^c+1,
+      then [log2_up (a*b) = c+c +1] while [(log2_up a) = (log2_up b) = c+1]
+*)
+
+(** At least, we get back the usual equation when we multiply by 2 (or 2^k) *)
+
+Lemma log2_up_mul_pow2 : forall a b, 0<a -> 0<=b ->
+ log2_up (a*2^b) == b + log2_up a.
+Proof.
+ intros a b Ha Hb.
+ rewrite <- le_succ_l, <- one_succ in Ha; le_elim Ha.
+ apply log2_up_unique. apply add_nonneg_pos; trivial. now apply log2_up_pos.
+ split.
+ assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)).
+ rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial.
+ apply mul_lt_mono_pos_r. order_pos. now apply log2_up_spec.
+ rewrite <- lt_succ_r, EQ. now apply log2_up_pos.
+ rewrite pow_add_r, mul_comm; trivial.
+ apply mul_le_mono_nonneg_l. order_pos. now apply log2_up_spec.
+ apply log2_up_nonneg.
+ now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2.
+Qed.
+
+Lemma log2_up_double : forall a, 0<a -> log2_up (2*a) == S (log2_up a).
+Proof.
+ intros a Ha. generalize (log2_up_mul_pow2 a 1 Ha le_0_1). now nzsimpl'.
+Qed.
+
+(** Two numbers with same [log2_up] cannot be far away. *)
+
+Lemma log2_up_same : forall a b, 0<a -> 0<b -> log2_up a == log2_up b -> a < 2*b.
+Proof.
+ intros a b Ha Hb H.
+ apply log2_up_lt_cancel. rewrite log2_up_double, H by trivial.
+ apply lt_succ_diag_r.
+Qed.
+
+(** [log2_up] and successor :
+    - the [log2_up] function climbs by at most 1 at a time
+    - otherwise it stays at the same value
+    - the +1 steps occur after powers of two
+*)
+
+Lemma log2_up_succ_le : forall a, log2_up (S a) <= S (log2_up a).
+Proof.
+ intros a.
+ destruct (lt_trichotomy 1 a) as [LT|[EQ|LT]].
+ rewrite 2 log2_up_eqn; trivial.
+ rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1.
+ apply log2_succ_le.
+ apply lt_succ_r; order.
+ rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'.
+ rewrite 2 log2_up_eqn0. order_pos. order'. now rewrite le_succ_l.
+Qed.
+
+Lemma log2_up_succ_or : forall a,
+ log2_up (S a) == S (log2_up a) \/ log2_up (S a) == log2_up a.
+Proof.
+ intros.
+ destruct (le_gt_cases (log2_up (S a)) (log2_up a)).
+ right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order.
+ left. apply le_succ_l in H. generalize (log2_up_succ_le a); order.
+Qed.
+
+Lemma log2_up_eq_succ_is_pow2 : forall a,
+ log2_up (S a) == S (log2_up a) -> exists b, a == 2^b.
+Proof.
+ intros a H.
+ destruct (le_gt_cases a 0) as [Ha|Ha].
+ rewrite 2 (proj2 (log2_up_null _)) in H. generalize (lt_succ_diag_r 0); order.
+ order'. apply le_succ_l. order'.
+ assert (Ha' : 1 < S a) by (now rewrite one_succ, <- succ_lt_mono).
+ exists (log2_up a).
+ generalize (proj1 (log2_up_spec (S a) Ha')) (proj2 (log2_log2_up_spec a Ha)).
+ rewrite H, pred_succ, lt_succ_r. order.
+Qed.
+
+Lemma log2_up_eq_succ_iff_pow2 : forall a, 0<a ->
+ (log2_up (S a) == S (log2_up a) <-> exists b, a == 2^b).
+Proof.
+ intros a Ha.
+ split. apply log2_up_eq_succ_is_pow2.
+ intros (b,Hb).
+ destruct (lt_ge_cases b 0) as [Hb'|Hb'].
+  rewrite pow_neg_r in Hb; order.
+ rewrite Hb, log2_up_pow2; try order'.
+ now rewrite log2_up_succ_pow2.
+Qed.
+
+Lemma log2_up_succ_double : forall a, 0<a ->
+ log2_up (2*a+1) == 2 + log2 a.
+Proof.
+ intros a Ha.
+ rewrite log2_up_eqn. rewrite add_1_r, pred_succ, log2_double; now nzsimpl'.
+ apply le_lt_trans with (0+1). now nzsimpl'.
+ apply add_lt_mono_r. order_pos.
+Qed.
+
+(** [log2_up] and addition *)
+
+Lemma log2_up_add_le : forall a b, a~=1 -> b~=1 ->
+ log2_up (a+b) <= log2_up a + log2_up b.
+Proof.
+ intros a b Ha Hb.
+ destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|].
+ rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono.
+ rewrite one_succ, lt_succ_r in Ha'.
+ rewrite <- (add_0_l b) at 2. now apply add_le_mono.
+ destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|].
+ rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono.
+ rewrite one_succ, lt_succ_r in Hb'.
+ rewrite <- (add_0_r a) at 2. now apply add_le_mono.
+ clear Ha Hb.
+ transitivity (log2_up (a*b)).
+ now apply log2_up_le_mono, add_le_mul.
+ apply log2_up_mul_above; order'.
+Qed.
+
+(** The sum of two [log2_up] is less than twice the [log2_up] of the sum.
+    The large inequality is obvious thanks to monotonicity.
+    The strict one requires some more work. This is almost
+    a convexity inequality for points [2a], [2b] and their middle [a+b] :
+    ideally, we would have [2*log(a+b) >= log(2a)+log(2b) = 2+log a+log b].
+    Here, we cannot do better: consider for instance a=3 b=5, then 2+3<2*3
+*)
+
+Lemma add_log2_up_lt : forall a b, 0<a -> 0<b ->
+ log2_up a + log2_up b < 2 * log2_up (a+b).
+Proof.
+ intros a b Ha Hb. nzsimpl'.
+ assert (H : log2_up a <= log2_up (a+b)).
+  apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order.
+ assert (H' : log2_up b <= log2_up (a+b)).
+  apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
+ le_elim H.
+ apply lt_le_trans with (log2_up (a+b) + log2_up b).
+  now apply add_lt_mono_r. now apply add_le_mono_l.
+ rewrite <- H at 1. apply add_lt_mono_l.
+ le_elim H'. trivial.
+ symmetry in H. apply log2_up_same in H; try order_pos.
+ symmetry in H'. apply log2_up_same in H'; try order_pos.
+ revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order.
+Qed.
+
+End NZLog2UpProp.
+
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index b1adcea9..2b5a1cf3 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,13 +8,10 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NZMul.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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.
@@ -59,12 +56,34 @@ Qed.
 
 Theorem mul_1_l : forall n, 1 * n == n.
 Proof.
-intro n. now nzsimpl.
+intro n. now nzsimpl'.
 Qed.
 
 Theorem mul_1_r : forall n, n * 1 == n.
 Proof.
-intro n. now nzsimpl.
+intro n. now nzsimpl'.
+Qed.
+
+Hint Rewrite mul_1_l mul_1_r : nz.
+
+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.
+
+Theorem mul_shuffle3 : forall n m p, n * (m * p) == m * (n * p).
+Proof.
+intros n m p. now rewrite mul_assoc, (mul_comm n), mul_assoc.
 Qed.
 
-End NZMulPropSig.
+End NZMulProp.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 09e468ff..97306f93 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,13 +8,11 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NZMulOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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).
@@ -26,17 +24,16 @@ Qed.
 
 Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m).
 Proof.
-nzord_induct p.
-intros n m H; false_hyp H lt_irrefl.
-intros p H IH n m H1. nzsimpl.
-le_elim H. assert (LR : forall n m, n < m -> p * n + n < p * m + m).
-intros n1 m1 H2. apply add_lt_mono; [now apply -> IH | assumption].
-split; [apply LR |]. intro H2. apply -> lt_dne; intro H3.
-apply <- le_ngt in H3. le_elim H3.
-apply lt_asymm in H2. apply H2. now apply LR.
-rewrite H3 in H2; false_hyp H2 lt_irrefl.
-rewrite <- H; now nzsimpl.
-intros p H1 _ n m H2. destruct (lt_asymm _ _ H1 H2).
+intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). solve_proper.
+intros. now nzsimpl.
+clear p Hp. intros p Hp IH n m. nzsimpl.
+assert (LR : forall n m, n < m -> p * n + n < p * m + m)
+ by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH).
+split; intros H.
+now apply LR.
+destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
+rewrite EQ in H. order.
+apply LR in GT. order.
 Qed.
 
 Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p).
@@ -48,19 +45,19 @@ Qed.
 Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n).
 Proof.
 nzord_induct p.
-intros n m H; false_hyp H lt_irrefl.
-intros p H1 _ n m H2. apply lt_succ_l in H2. apply <- nle_gt in H2.
-false_hyp H1 H2.
-intros p H IH n m H1. apply <- le_succ_l in H.
-le_elim H. assert (LR : forall n m, n < m -> p * m < p * n).
-intros n1 m1 H2. apply (le_lt_add_lt n1 m1).
-now apply lt_le_incl. rewrite <- 2 mul_succ_l. now apply -> IH.
-split; [apply LR |]. intro H2. apply -> lt_dne; intro H3.
-apply <- le_ngt in H3. le_elim H3.
-apply lt_asymm in H2. apply H2. now apply LR.
-rewrite H3 in H2; false_hyp H2 lt_irrefl.
-rewrite (mul_lt_pred p (S p)) by reflexivity.
-rewrite H; do 2 rewrite mul_0_l; now do 2 rewrite add_0_l.
+order.
+intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order.
+intros p Hp IH n m _. apply le_succ_l in Hp.
+le_elim Hp.
+assert (LR : forall n m, n < m -> p * m < p * n).
+ intros n1 m1 H. apply (le_lt_add_lt n1 m1).
+ now apply lt_le_incl. rewrite <- 2 mul_succ_l. now rewrite <- IH.
+split; intros H.
+now apply LR.
+destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
+rewrite EQ in H. order.
+apply LR in GT. order.
+rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl.
 Qed.
 
 Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p).
@@ -72,7 +69,7 @@ Qed.
 Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_pos_l.
+le_elim H2. apply lt_le_incl. now apply mul_lt_mono_pos_l.
 apply eq_le_incl; now rewrite H2.
 apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l.
 Qed.
@@ -80,7 +77,7 @@ Qed.
 Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n.
 Proof.
 intros n m p H1 H2. le_elim H1.
-le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_neg_l.
+le_elim H2. apply lt_le_incl. now apply mul_lt_mono_neg_l.
 apply eq_le_incl; now rewrite H2.
 apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l.
 Qed.
@@ -99,20 +96,13 @@ Qed.
 
 Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof.
-intros n m p H; split; intro H1.
-destruct (lt_trichotomy p 0) as [H2 | [H2 | H2]].
-apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * m < p * n); [now apply -> mul_lt_mono_neg_l |].
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-assert (H4 : p * n < p * m); [now apply -> mul_lt_mono_neg_l |].
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-false_hyp H2 H.
-apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m) by (now apply -> mul_lt_mono_pos_l).
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-assert (H4 : p * m < p * n) by (now apply -> mul_lt_mono_pos_l).
-rewrite H1 in H4; false_hyp H4 lt_irrefl.
-now rewrite H1.
+intros n m p Hp; split; intro H; [|now f_equiv].
+apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp];
+ destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
+apply (mul_lt_mono_neg_l p) in LT; order.
+apply (mul_lt_mono_neg_l p) in GT; order.
+apply (mul_lt_mono_pos_l p) in LT; order.
+apply (mul_lt_mono_pos_l p) in GT; order.
 Qed.
 
 Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m).
@@ -183,17 +173,17 @@ Qed.
 
 Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m.
 Proof.
-intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_pos_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_pos_r.
 Qed.
 
 Theorem mul_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m.
 Proof.
-intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r.
 Qed.
 
 Theorem mul_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r.
+intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r.
 Qed.
 
 Theorem mul_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0.
@@ -206,9 +196,33 @@ Proof.
 intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order.
 Qed.
 
+Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m).
+Proof.
+intros n m Hn. rewrite <- (mul_0_r n) at 1.
+ symmetry. now apply mul_lt_mono_pos_l.
+Qed.
+
+Theorem mul_pos_cancel_r : forall n m, 0 < m -> (0 < n*m <-> 0 < n).
+Proof.
+intros n m Hn. rewrite <- (mul_0_l m) at 1.
+ symmetry. now apply mul_lt_mono_pos_r.
+Qed.
+
+Theorem mul_nonneg_cancel_l : forall n m, 0 < n -> (0 <= n*m <-> 0 <= m).
+Proof.
+intros n m Hn. rewrite <- (mul_0_r n) at 1.
+ symmetry. now apply mul_le_mono_pos_l.
+Qed.
+
+Theorem mul_nonneg_cancel_r : forall n m, 0 < m -> (0 <= n*m <-> 0 <= n).
+Proof.
+intros n m Hn. rewrite <- (mul_0_l m) at 1.
+ symmetry. now apply mul_le_mono_pos_r.
+Qed.
+
 Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m.
 Proof.
-intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1.
+intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1.
 rewrite mul_1_l in H1. now apply lt_1_l with m.
 assumption.
 Qed.
@@ -229,7 +243,7 @@ Qed.
 Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof.
 intros n m; split; intro H.
-intro H1; apply -> eq_mul_0 in H1. tauto.
+intro H1; apply eq_mul_0 in H1. tauto.
 split; intro H1; rewrite H1 in H;
 (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H.
 Qed.
@@ -241,16 +255,22 @@ Qed.
 
 Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0.
 Proof.
-intros n m H1 H2. apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2. apply eq_mul_0 in H1. destruct H1 as [H1 | H1].
 assumption. false_hyp H1 H2.
 Qed.
 
 Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0.
 Proof.
-intros n m H1 H2; apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1].
+intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1].
 false_hyp H1 H2. assumption.
 Qed.
 
+(** Some alternative names: *)
+
+Definition mul_eq_0 := eq_mul_0.
+Definition mul_eq_0_l := eq_mul_0_l.
+Definition mul_eq_0_r := eq_mul_0_r.
+
 Theorem lt_0_mul : forall n m, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0).
 Proof.
 intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
@@ -283,25 +303,100 @@ Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m.
 Proof.
 intros n m H1 H2. destruct (lt_ge_cases n 0).
 now apply lt_le_trans with 0.
-destruct (lt_ge_cases n m).
-assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonneg.
-apply -> le_ngt in F. false_hyp H2 F.
+destruct (lt_ge_cases n m) as [LT|LE]; trivial.
+apply square_le_mono_nonneg in LE; order.
 Qed.
 
 Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m.
 Proof.
 intros n m H1 H2. destruct (lt_ge_cases n 0).
 apply lt_le_incl; now apply lt_le_trans with 0.
-destruct (le_gt_cases n m).
-assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonneg.
-apply -> lt_nge in F. false_hyp H2 F.
+destruct (le_gt_cases n m) as [LE|LT]; trivial.
+apply square_lt_mono_nonneg in LT; order.
+Qed.
+
+Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m.
+Proof.
+intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two).
+rewrite two_succ. nzsimpl. now rewrite le_succ_l.
+order'.
+Qed.
+
+Lemma add_le_mul : forall a b, 1<a -> 1<b -> a+b <= a*b.
+Proof.
+ assert (AUX : forall a b, 0<a -> 0<b -> (S a)+(S b) <= (S a)*(S b)).
+  intros a b Ha Hb.
+  nzsimpl. rewrite <- succ_le_mono. apply le_succ_l.
+  rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b).
+  apply add_lt_mono_r.
+  now apply mul_pos_pos.
+ intros a b Ha Hb.
+ assert (Ha' := lt_succ_pred 1 a Ha).
+ assert (Hb' := lt_succ_pred 1 b Hb).
+ rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order.
+Qed.
+
+(** A few results about squares *)
+
+Lemma square_nonneg : forall a, 0 <= a * a.
+Proof.
+ intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0).
+ now apply mul_le_mono_nonpos_l.
+ apply mul_le_mono_nonneg_l; order.
+Qed.
+
+Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b.
+Proof.
+ assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b).
+  intros a b (Ha,H).
+  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. order.
+ intros a b Ha Hb.
+ destruct (le_gt_cases a b).
+ apply AUX; split; order.
+ rewrite (add_comm (b*a)), (add_comm (a*a)).
+ apply AUX; split; order.
+Qed.
+
+Lemma add_square_le : forall a b, 0<=a -> 0<=b ->
+ a*a + b*b <= (a+b)*(a+b).
+Proof.
+ intros a b Ha Hb.
+ rewrite mul_add_distr_r, !mul_add_distr_l.
+ rewrite add_assoc.
+ apply add_le_mono_r.
+ rewrite <- add_assoc.
+ rewrite <- (add_0_r (a*a)) at 1.
+ apply add_le_mono_l.
+ apply add_nonneg_nonneg; now apply mul_nonneg_nonneg.
+Qed.
+
+Lemma square_add_le : forall a b, 0<=a -> 0<=b ->
+ (a+b)*(a+b) <= 2*(a*a + b*b).
+Proof.
+ intros a b Ha Hb.
+ 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.
+ apply crossmul_le_addsquare; order.
 Qed.
 
-Theorem mul_2_mono_l : forall n m, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b ->
+ 2*2*a*b <= (a+b)*(a+b).
 Proof.
-intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m (1 + 1)).
-rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l.
-apply add_pos_pos; now apply lt_0_1.
+ intros.
+ nzsimpl'.
+ rewrite !mul_add_distr_l, !mul_add_distr_r.
+ rewrite (add_comm _ (b*b)), add_assoc.
+ apply add_le_mono_r.
+ rewrite (add_shuffle0 (a*a)), (mul_comm b a).
+ apply add_le_mono_r.
+ rewrite (mul_comm a b) at 1.
+ now apply crossmul_le_addsquare.
 Qed.
 
-End NZMulOrderPropSig.
+End NZMulOrderProp.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 07805772..8cf5b26f 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,28 +8,26 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NZOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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.
-intros n n' Hn m m' Hm. rewrite !lt_eq_cases, !Hn, !Hm; auto with *.
+intros n n' Hn m m' Hm. now rewrite <- !lt_succ_r, Hn, Hm.
 Qed.
 
 Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H].
 
 Theorem lt_le_incl : forall n m, n < m -> n <= m.
 Proof.
-intros; apply <- lt_eq_cases; now left.
+intros. apply lt_eq_cases. now left.
 Qed.
 
 Theorem le_refl : forall n, n <= n.
 Proof.
-intro; apply <- lt_eq_cases; now right.
+intro. apply lt_eq_cases. now right.
 Qed.
 
 Theorem lt_succ_diag_r : forall n, n < S n.
@@ -99,7 +97,7 @@ intros n m; nzinduct n m.
 intros H; false_hyp H lt_irrefl.
 intro n; split; intros H H1 H2.
 apply lt_succ_r in H2. le_elim H2.
-apply H; auto. apply -> le_succ_l. now apply lt_le_incl.
+apply H; auto. apply le_succ_l. now apply lt_le_incl.
 rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l.
 apply le_succ_l in H1. le_elim H1.
 apply H; auto. rewrite lt_succ_r. now apply lt_le_incl.
@@ -148,7 +146,8 @@ Definition lt_compat := lt_wd.
 Definition lt_total := lt_trichotomy.
 Definition le_lteq := lt_eq_cases.
 
-Module OrderElts <: TotalOrder.
+Module Private_OrderTac.
+Module Elts <: TotalOrder.
  Definition t := t.
  Definition eq := eq.
  Definition lt := lt.
@@ -158,9 +157,10 @@ Module OrderElts <: TotalOrder.
  Definition lt_compat := lt_compat.
  Definition lt_total := lt_total.
  Definition le_lteq := le_lteq.
-End OrderElts.
-Module OrderTac := !MakeOrderTac OrderElts.
-Ltac order := OrderTac.order.
+End Elts.
+Module Tac := !MakeOrderTac Elts.
+End Private_OrderTac.
+Ltac order := Private_OrderTac.Tac.order.
 
 (** Some direct consequences of [order]. *)
 
@@ -208,12 +208,12 @@ Qed.
 
 Theorem lt_succ_l : forall n m, S n < m -> n < m.
 Proof.
-intros n m H; apply -> le_succ_l; order.
+intros n m H; apply le_succ_l; order.
 Qed.
 
 Theorem le_le_succ_r : forall n m, n <= m -> n <= S m.
 Proof.
-intros n m LE. rewrite <- lt_succ_r in LE. order.
+intros n m LE. apply lt_succ_r in LE. order.
 Qed.
 
 Theorem lt_lt_succ_r : forall n m, n < m -> n < S m.
@@ -233,19 +233,37 @@ Qed.
 
 Theorem lt_0_1 : 0 < 1.
 Proof.
-apply lt_succ_diag_r.
+rewrite one_succ. apply lt_succ_diag_r.
 Qed.
 
 Theorem le_0_1 : 0 <= 1.
 Proof.
-apply le_succ_diag_r.
+apply lt_le_incl, lt_0_1.
 Qed.
 
-Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
+Theorem lt_1_2 : 1 < 2.
+Proof.
+rewrite two_succ. apply lt_succ_diag_r.
+Qed.
+
+Theorem lt_0_2 : 0 < 2.
+Proof.
+transitivity 1. apply lt_0_1. apply lt_1_2.
+Qed.
+
+Theorem le_0_2 : 0 <= 2.
 Proof.
-intros n m H1 H2. apply <- le_succ_l in H1. order.
+apply lt_le_incl, lt_0_2.
 Qed.
 
+(** The order tactic enriched with some knowledge of 0,1,2 *)
+
+Ltac order' := generalize lt_0_1 lt_1_2; order.
+
+Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
+Proof.
+intros n m H1 H2. rewrite <- le_succ_l, <- one_succ in H1. order.
+Qed.
 
 (** More Trichotomy, decidability and double negation elimination. *)
 
@@ -347,7 +365,7 @@ Proof.
 intro z; nzinduct n z.
 order.
 intro n; split; intros IH m H1 H2.
-apply -> le_succ_r in H2. destruct H2 as [H2 | H2].
+apply le_succ_r in H2. destruct H2 as [H2 | H2].
 now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2].
 apply IH. assumption. now apply le_le_succ_r.
 Qed.
@@ -359,6 +377,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 *)
 
@@ -390,14 +415,14 @@ Qed.
 Lemma rs'_rs'' : right_step' -> right_step''.
 Proof.
 intros RS' n; split; intros H1 m H2 H3.
-apply -> lt_succ_r in H3; le_elim H3;
+apply lt_succ_r in H3; le_elim H3;
 [now apply H1 | rewrite H3 in *; now apply RS'].
 apply H1; [assumption | now apply lt_lt_succ_r].
 Qed.
 
 Lemma rbase : A' z.
 Proof.
-intros m H1 H2. apply -> le_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply le_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n.
@@ -449,28 +474,28 @@ Let left_step'' := forall n, A' n <-> A' (S n).
 Lemma ls_ls' :  A z -> left_step -> left_step'.
 Proof.
 intros Az LS n H1 H2. le_elim H1.
-apply LS; trivial. apply H2; [now apply <- le_succ_l | now apply eq_le_incl].
+apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl].
 rewrite H1; apply Az.
 Qed.
 
 Lemma ls'_ls'' : left_step' -> left_step''.
 Proof.
 intros LS' n; split; intros H1 m H2 H3.
-apply -> le_succ_l in H3. apply lt_le_incl in H3. now apply H1.
+apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1.
 le_elim H3.
-apply <- le_succ_l in H3. now apply H1.
+apply le_succ_l in H3. now apply H1.
 rewrite <- H3 in *; now apply LS'.
 Qed.
 
 Lemma lbase : A' (S z).
 Proof.
-intros m H1 H2. apply -> le_succ_l in H2.
-apply -> le_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply le_succ_l in H2.
+apply le_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma A'A_left : (forall n, A' n) -> forall n, n <= z -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := n); [assumption | now apply eq_le_incl].
+intros H1 n H2. apply (H1 n); [assumption | now apply eq_le_incl].
 Qed.
 
 Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.
@@ -527,8 +552,8 @@ Theorem order_induction' :
     forall n, A n.
 Proof.
 intros Az AS AP n; apply order_induction; try assumption.
-intros m H1 H2. apply AP in H2; [| now apply <- le_succ_l].
-apply -> (A_wd (P (S m)) m); [assumption | apply pred_succ].
+intros m H1 H2. apply AP in H2; [|now apply le_succ_l].
+now rewrite pred_succ in H2.
 Qed.
 
 End Center.
@@ -555,11 +580,11 @@ Theorem lt_ind : forall (n : t),
    forall m, n < m -> A m.
 Proof.
 intros n H1 H2 m H3.
-apply right_induction with (S n); [assumption | | now apply <- le_succ_l].
-intros; apply H2; try assumption. now apply -> le_succ_l.
+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 ->
@@ -582,8 +607,8 @@ Section WF.
 
 Variable z : t.
 
-Let Rlt (n m : t) := z <= n /\ n < m.
-Let Rgt (n m : t) := m < n /\ n <= z.
+Let Rlt (n m : t) := z <= n < m.
+Let Rgt (n m : t) := m < n <= z.
 
 Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt.
 Proof.
@@ -595,25 +620,13 @@ Proof.
 intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2.
 Qed.
 
-Instance Acc_lt_wd : Proper (eq==>iff) (Acc Rlt).
-Proof.
-intros x1 x2 H; split; intro H1; destruct H1 as [H2];
-constructor; intros; apply H2; now (rewrite H || rewrite <- H).
-Qed.
-
-Instance Acc_gt_wd : Proper (eq==>iff) (Acc Rgt).
-Proof.
-intros x1 x2 H; split; intro H1; destruct H1 as [H2];
-constructor; intros; apply H2; now (rewrite H || rewrite <- H).
-Qed.
-
 Theorem lt_wf : well_founded Rlt.
 Proof.
 unfold well_founded.
 apply strong_right_induction' with (z := z).
-apply Acc_lt_wd.
+auto with typeclass_instances.
 intros n H; constructor; intros y [H1 H2].
-apply <- nle_gt in H2. elim H2. now apply le_trans with z.
+apply nle_gt in H2. elim H2. now apply le_trans with z.
 intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
 Qed.
 
@@ -621,24 +634,20 @@ Theorem gt_wf : well_founded Rgt.
 Proof.
 unfold well_founded.
 apply strong_left_induction' with (z := z).
-apply Acc_gt_wd.
+auto with typeclass_instances.
 intros n H; constructor; intros y [H1 H2].
-apply <- nle_gt in H2. elim H2. now apply le_lt_trans with n.
+apply nle_gt in H2. elim H2. now apply le_lt_trans with n.
 intros n H1 H2; constructor; intros m [H3 H4].
-apply H2. assumption. now apply <- le_succ_l.
+apply H2. assumption. now apply le_succ_l.
 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/NZParity.v b/theories/Numbers/NatInt/NZParity.v
new file mode 100644
index 00000000..29109ccb
--- /dev/null
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -0,0 +1,263 @@
+(************************************************************************)
+(*  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 NZAxioms NZMulOrder.
+
+(** Parity functions *)
+
+Module Type NZParity (Import A : NZAxiomsSig').
+ 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 NZParity.
+
+Module Type NZParityProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZParity A)
+ (Import C : NZMulOrderProp A).
+
+(** Morphisms *)
+
+Instance Even_wd : Proper (eq==>iff) Even.
+Proof. unfold Even. solve_proper. Qed.
+
+Instance Odd_wd : Proper (eq==>iff) Odd.
+Proof. unfold Odd. solve_proper. Qed.
+
+Instance even_wd : Proper (eq==>Logic.eq) even.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now f_equiv.
+Qed.
+
+Instance odd_wd : Proper (eq==>Logic.eq) odd.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now f_equiv.
+Qed.
+
+(** Evenness and oddity are dual notions *)
+
+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.
+ assert (LT : exists z, z<y).
+  destruct (lt_ge_cases 0 y) as [LT|GT]; [now exists 0 | exists x].
+  rewrite <- le_succ_l, H. nzsimpl'.
+  rewrite <- (add_0_r y) at 3. now apply add_le_mono_l.
+ destruct LT as (z,LT).
+ destruct (lt_exists_pred z y LT) as (y' & Hy' & _).
+ exists y'. rewrite <- succ_inj_wd, H, Hy'. now nzsimpl'.
+ 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 : 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 : forall n, negb (even n) = odd n.
+Proof.
+ intros. rewrite <- negb_odd. apply negb_involutive.
+Qed.
+
+(** Constants *)
+
+Lemma even_0 : even 0 = true.
+Proof.
+ rewrite even_spec. exists 0. now nzsimpl.
+Qed.
+
+Lemma odd_0 : odd 0 = false.
+Proof.
+ now rewrite <- negb_even, even_0.
+Qed.
+
+Lemma odd_1 : odd 1 = true.
+Proof.
+ rewrite odd_spec. exists 0. now nzsimpl'.
+Qed.
+
+Lemma even_1 : even 1 = false.
+Proof.
+ now rewrite <- negb_odd, odd_1.
+Qed.
+
+Lemma even_2 : even 2 = true.
+Proof.
+ rewrite even_spec. exists 1. now nzsimpl'.
+Qed.
+
+Lemma odd_2 : odd 2 = false.
+Proof.
+ now rewrite <- negb_even, even_2.
+Qed.
+
+(** Parity and successor *)
+
+Lemma Odd_succ : 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 f_equiv.
+Qed.
+
+Lemma odd_succ : forall n, odd (S n) = even n.
+Proof.
+ intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec.
+ apply Odd_succ.
+Qed.
+
+Lemma even_succ : forall n, even (S n) = odd n.
+Proof.
+ intros. now rewrite <- negb_odd, odd_succ, negb_even.
+Qed.
+
+Lemma Even_succ : forall n, Even (S n) <-> Odd n.
+Proof.
+ intros. now rewrite <- even_spec, even_succ, odd_spec.
+Qed.
+
+(** Parity and successor of successor *)
+
+Lemma Even_succ_succ : forall n, Even (S (S n)) <-> Even n.
+Proof.
+ intros. now rewrite Even_succ, Odd_succ.
+Qed.
+
+Lemma Odd_succ_succ : forall n, Odd (S (S n)) <-> Odd n.
+Proof.
+ intros. now rewrite Odd_succ, Even_succ.
+Qed.
+
+Lemma even_succ_succ : forall n, even (S (S n)) = even n.
+Proof.
+ intros. now rewrite even_succ, odd_succ.
+Qed.
+
+Lemma odd_succ_succ : forall n, odd (S (S n)) = odd n.
+Proof.
+ intros. now rewrite odd_succ, even_succ.
+Qed.
+
+(** Parity and addition *)
+
+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_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. rewrite even_add.
+ now destruct (even n), (even m).
+Qed.
+
+(** Parity and multiplication *)
+
+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_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. rewrite even_mul.
+ now destruct (even n), (even m).
+Qed.
+
+(** A particular case : adding by an even number *)
+
+Lemma even_add_even : forall n m, Even m -> even (n+m) = even n.
+Proof.
+ intros n m Hm. apply even_spec in Hm.
+ rewrite even_add, Hm. now destruct (even n).
+Qed.
+
+Lemma odd_add_even : forall n m, Even m -> odd (n+m) = odd n.
+Proof.
+ intros n m Hm. apply even_spec in Hm.
+ rewrite odd_add, <- (negb_even m), Hm. now destruct (odd n).
+Qed.
+
+Lemma even_add_mul_even : forall n m p, Even m -> even (n+m*p) = even n.
+Proof.
+ intros n m p Hm. apply even_spec in Hm.
+ apply even_add_even. apply even_spec. now rewrite even_mul, Hm.
+Qed.
+
+Lemma odd_add_mul_even : forall n m p, Even m -> odd (n+m*p) = odd n.
+Proof.
+ intros n m p Hm. apply even_spec in Hm.
+ apply odd_add_even. apply even_spec. now rewrite even_mul, Hm.
+Qed.
+
+Lemma even_add_mul_2 : forall n m, even (n+2*m) = even n.
+Proof.
+ intros. apply even_add_mul_even. apply even_spec, even_2.
+Qed.
+
+Lemma odd_add_mul_2 : forall n m, odd (n+2*m) = odd n.
+Proof.
+ intros. apply odd_add_mul_even. apply even_spec, even_2.
+Qed.
+
+End NZParityProp.
\ No newline at end of file
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
new file mode 100644
index 00000000..58704735
--- /dev/null
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -0,0 +1,411 @@
+(************************************************************************)
+(*  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 A : Typ).
+ Parameters Inline pow : t -> t -> t.
+End Pow.
+
+Module Type PowNotation (A : Typ)(Import B : Pow A).
+ Infix "^" := pow.
+End PowNotation.
+
+Module Type Pow' (A : Typ) := Pow A <+ PowNotation A.
+
+Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A).
+ 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.
+ Axiom pow_neg_r : forall a b, b<0 -> a^b == 0.
+End NZPowSpec.
+
+(** The above [pow_neg_r] specification is useless (and trivially
+   provable) for N. Having it here allows to already derive
+   some slightly more general statements. *)
+
+Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A.
+Module Type NZPow' (A : NZOrdAxiomsSig) := Pow' A <+ NZPowSpec A.
+
+(** Derived properties of power *)
+
+Module Type NZPowProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZPow' A)
+ (Import C : NZMulOrderProp A).
+
+Hint Rewrite pow_0_r pow_succ_r : nz.
+
+(** 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_0_l' : forall a, a~=0 -> 0^a == 0.
+Proof.
+ intros a Ha.
+ destruct (lt_trichotomy a 0) as [LT|[EQ|GT]]; try order.
+ now rewrite pow_neg_r.
+ now apply pow_0_l.
+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_proper.
+ now nzsimpl.
+ now nzsimpl.
+Qed.
+
+Hint Rewrite pow_1_r pow_1_l : nz.
+
+Lemma pow_2_r : forall a, a^2 == a*a.
+Proof.
+ intros. rewrite two_succ. nzsimpl; order'.
+Qed.
+
+Hint Rewrite pow_2_r : nz.
+
+(** Power and nullity *)
+
+Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0.
+Proof.
+ intros a b Hb. apply le_ind with (4:=Hb).
+ solve_proper.
+ rewrite pow_0_r. order'.
+ clear b Hb. intros b Hb IH.
+ rewrite pow_succ_r by trivial.
+ intros H. apply eq_mul_0 in H. destruct H; trivial.
+ now apply IH.
+Qed.
+
+Lemma pow_nonzero : forall a b, a~=0 -> 0<=b -> a^b ~= 0.
+Proof.
+ intros a b Ha Hb. contradict Ha. now apply pow_eq_0 with b.
+Qed.
+
+Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0<b /\ a==0).
+Proof.
+ intros a b. split.
+ intros H.
+ destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]].
+ now left.
+ rewrite Hb, pow_0_r in H; order'.
+ right. split; trivial. apply pow_eq_0 with b; order.
+ intros [Hb|[Hb Ha]]. now rewrite pow_neg_r.
+ rewrite Ha. apply pow_0_l'. 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_proper.
+ 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,
+  (a*b)^c == a^c * b^c.
+Proof.
+ intros a b c.
+ destruct (lt_ge_cases c 0) as [Hc|Hc].
+ rewrite !(pow_neg_r _ _ Hc). now nzsimpl.
+ apply le_ind with (4:=Hc). solve_proper.
+ 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_proper.
+ 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 : forall a b, 0<=a -> 0<=a^b.
+Proof.
+ intros a b Ha.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ now rewrite !(pow_neg_r _ _ Hb).
+ apply le_ind with (4:=Hb). solve_proper.
+ 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_proper.
+ 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_proper.
+ 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; try order.
+ apply IH. now split.
+Qed.
+
+Lemma pow_le_mono_l : forall a b c, 0<=a<=b -> a^c <= b^c.
+Proof.
+ intros a b c (Ha,H).
+ destruct (lt_trichotomy c 0) as [Hc|[Hc|Hc]].
+ rewrite !(pow_neg_r _ _ Hc); now nzsimpl.
+ rewrite Hc; now nzsimpl.
+ 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.
+Qed.
+
+Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b).
+Proof.
+ intros a b Ha. split; intros Hb.
+ rewrite <- (pow_1_l b) by order.
+ apply pow_lt_mono_l; try split; order'.
+ destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial.
+ rewrite pow_neg_r in Hb; order'.
+ rewrite H, pow_0_r in Hb. order.
+Qed.
+
+Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=c -> b<c -> a^b < a^c.
+Proof.
+ intros a b c Ha Hc H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'.
+ 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 -> b<=c -> a^b <= a^c.
+Proof.
+ intros a b c Ha H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order.
+ apply le_succ_l in Ha; rewrite <- one_succ 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; order.
+ nzsimpl; order.
+Qed.
+
+Lemma pow_le_mono : forall a b c d, 0<a<=c -> 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; rewrite <- one_succ 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.
+ 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<=c ->
+  (b<c <-> a^b < a^c).
+Proof.
+ intros a b c Ha Hc.
+ split; intro LT.
+ now apply pow_lt_mono_r.
+ destruct (le_gt_cases c b) as [LE|GT]; trivial.
+ assert (a^c <= a^b) by (apply pow_le_mono_r; order').
+ order.
+Qed.
+
+Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c ->
+  (b<=c <-> a^b <= a^c).
+Proof.
+ intros a b c Ha Hc.
+ split; intro LE.
+ apply pow_le_mono_r; order'.
+ destruct (le_gt_cases b c) as [LE'|GT]; trivial.
+ assert (a^c < a^b) by (apply pow_lt_mono_r; 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_proper.
+ nzsimpl. order'.
+ clear b Hb. intros b Hb IH. nzsimpl; trivial.
+ rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha.
+ 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_proper.
+ 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; trivial.
+ rewrite <- add_0_l at 1. apply add_le_mono_r.
+  apply mul_nonneg_nonneg; trivial.
+  apply pow_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_proper.
+ 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; 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 7279325d..13c26233 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
@@ -8,13 +8,11 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NZProperties.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
new file mode 100644
index 00000000..6e85c689
--- /dev/null
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -0,0 +1,734 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Square Root Function *)
+
+Require Import NZAxioms NZMulOrder.
+
+(** Interface of a sqrt function, then its specification on naturals *)
+
+Module Type Sqrt (Import A : Typ).
+ Parameter Inline sqrt : t -> t.
+End Sqrt.
+
+Module Type SqrtNotation (A : Typ)(Import B : Sqrt A).
+ Notation "√ x" := (sqrt x) (at level 6).
+End SqrtNotation.
+
+Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A.
+
+Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A).
+ Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a).
+ Axiom sqrt_neg : forall a, a<0 -> √a == 0.
+End NZSqrtSpec.
+
+Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A.
+Module Type NZSqrt' (A : NZOrdAxiomsSig) := Sqrt' A <+ NZSqrtSpec A.
+
+(** Derived properties of power *)
+
+Module Type NZSqrtProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZSqrt' A)
+ (Import C : NZMulOrderProp A).
+
+Local Notation "a ²" := (a*a) (at level 5, no associativity, format "a ²").
+
+(** First, sqrt is non-negative *)
+
+Lemma sqrt_spec_nonneg : forall b,
+ b² < (S b)² -> 0 <= b.
+Proof.
+ intros b LT.
+ destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso.
+ assert ((S b)² < b²).
+  rewrite mul_succ_l, <- (add_0_r b²).
+  apply add_lt_le_mono.
+  apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r.
+  now apply le_succ_l.
+ order.
+Qed.
+
+Lemma sqrt_nonneg : forall a, 0<=√a.
+Proof.
+ intros. destruct (lt_ge_cases a 0) as [Ha|Ha].
+ now rewrite (sqrt_neg _ Ha).
+ apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order.
+Qed.
+
+(** The spec of sqrt indeed determines it *)
+
+Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b.
+Proof.
+ intros a b (LEb,LTb).
+ assert (Ha : 0<=a) by (transitivity b²; trivial using square_nonneg).
+ assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order).
+ assert (Ha': 0<=√a) by now apply sqrt_nonneg.
+ destruct (sqrt_spec a Ha) as (LEa,LTa).
+ assert (b <= √a).
+  apply lt_succ_r, square_lt_simpl_nonneg; [|order].
+  now apply lt_le_incl, lt_succ_r.
+ assert (√a <= b).
+  apply lt_succ_r, square_lt_simpl_nonneg; [|order].
+  now apply lt_le_incl, lt_succ_r.
+ order.
+Qed.
+
+(** Hence sqrt is a morphism *)
+
+Instance sqrt_wd : Proper (eq==>eq) sqrt.
+Proof.
+ intros x x' Hx.
+ destruct (lt_ge_cases x 0) as [H|H].
+ rewrite 2 sqrt_neg; trivial. reflexivity.
+ now rewrite <- Hx.
+ apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec.
+Qed.
+
+(** An alternate specification *)
+
+Lemma sqrt_spec_alt : forall a, 0<=a -> exists r,
+ a == (√a)² + r /\ 0 <= r <= 2*√a.
+Proof.
+ intros a Ha.
+ destruct (sqrt_spec _ Ha) as (LE,LT).
+ destruct (le_exists_sub _ _ LE) as (r & Hr & Hr').
+ exists r.
+ split. now rewrite add_comm.
+ split. trivial.
+ apply (add_le_mono_r _ _ (√a)²).
+ rewrite <- Hr, add_comm.
+ generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc.
+Qed.
+
+Lemma sqrt_unique' : forall a b c, 0<=c<=2*b ->
+ a == b² + c -> √a == b.
+Proof.
+ intros a b c (Hc,H) EQ.
+ apply sqrt_unique.
+ rewrite EQ.
+ split.
+ rewrite <- add_0_r at 1. now apply add_le_mono_l.
+ nzsimpl. apply lt_succ_r.
+ rewrite <- add_assoc. apply add_le_mono_l.
+ generalize H; now nzsimpl'.
+Qed.
+
+(** Sqrt is exact on squares *)
+
+Lemma sqrt_square : forall a, 0<=a -> √(a²) == a.
+Proof.
+ intros a Ha.
+ apply sqrt_unique' with 0.
+ split. order. apply mul_nonneg_nonneg; order'. now nzsimpl.
+Qed.
+
+(** Sqrt and predecessors of squares *)
+
+Lemma sqrt_pred_square : forall a, 0<a -> √(P a²) == P a.
+Proof.
+ intros a Ha.
+ apply sqrt_unique.
+ assert (EQ := lt_succ_pred 0 a Ha).
+ rewrite EQ. split.
+ apply lt_succ_r.
+ rewrite (lt_succ_pred 0).
+ assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ).
+ assert (P a < a) by (now rewrite <- le_succ_l, EQ).
+ apply mul_lt_mono_nonneg; trivial.
+ now apply mul_pos_pos.
+ apply le_succ_l.
+ rewrite (lt_succ_pred 0). reflexivity. now apply mul_pos_pos.
+Qed.
+
+(** Sqrt is a monotone function (but not a strict one) *)
+
+Lemma sqrt_le_mono : forall a b, a <= b -> √a <= √b.
+Proof.
+ intros a b Hab.
+ destruct (lt_ge_cases a 0) as [Ha|Ha].
+ rewrite (sqrt_neg _ Ha). apply sqrt_nonneg.
+ assert (Hb : 0 <= b) by order.
+ destruct (sqrt_spec a Ha) as (LE,_).
+ destruct (sqrt_spec b Hb) as (_,LT).
+ apply lt_succ_r.
+ apply square_lt_simpl_nonneg; try order.
+ now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+Qed.
+
+(** No reverse result for <=, consider for instance √2 <= √1 *)
+
+Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.
+Proof.
+ intros a b H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite (sqrt_neg b Hb) in H; generalize (sqrt_nonneg a); order.
+ destruct (lt_ge_cases a 0) as [Ha|Ha]; [order|].
+ destruct (sqrt_spec a Ha) as (_,LT).
+ destruct (sqrt_spec b Hb) as (LE,_).
+ apply le_succ_l in H.
+ assert ((S (√a))² <= (√b)²).
+  apply mul_le_mono_nonneg; trivial.
+  now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+  now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+ order.
+Qed.
+
+(** When left side is a square, we have an equivalence for <= *)
+
+Lemma sqrt_le_square : forall a b, 0<=a -> 0<=b -> (b²<=a <-> b <= √a).
+Proof.
+ intros a b Ha Hb. split; intros H.
+ rewrite <- (sqrt_square b); trivial.
+ now apply sqrt_le_mono.
+ destruct (sqrt_spec a Ha) as (LE,LT).
+ transitivity (√a)²; trivial.
+ now apply mul_le_mono_nonneg.
+Qed.
+
+(** When right side is a square, we have an equivalence for < *)
+
+Lemma sqrt_lt_square : forall a b, 0<=a -> 0<=b -> (a<b² <-> √a < b).
+Proof.
+ intros a b Ha Hb. split; intros H.
+ destruct (sqrt_spec a Ha) as (LE,_).
+ apply square_lt_simpl_nonneg; try order.
+ rewrite <- (sqrt_square b Hb) in H.
+ now apply sqrt_lt_cancel.
+Qed.
+
+(** Sqrt and basic constants *)
+
+Lemma sqrt_0 : √0 == 0.
+Proof.
+ rewrite <- (mul_0_l 0) at 1. now apply sqrt_square.
+Qed.
+
+Lemma sqrt_1 : √1 == 1.
+Proof.
+ rewrite <- (mul_1_l 1) at 1. apply sqrt_square. order'.
+Qed.
+
+Lemma sqrt_2 : √2 == 1.
+Proof.
+ apply sqrt_unique' with 1. nzsimpl; split; order'. now nzsimpl'.
+Qed.
+
+Lemma sqrt_pos : forall a, 0 < √a <-> 0 < a.
+Proof.
+ intros a. split; intros Ha. apply sqrt_lt_cancel. now rewrite sqrt_0.
+ rewrite <- le_succ_l, <- one_succ, <- sqrt_1. apply sqrt_le_mono.
+ now rewrite one_succ, le_succ_l.
+Qed.
+
+Lemma sqrt_lt_lin : forall a, 1<a -> √a<a.
+Proof.
+ intros a Ha. rewrite <- sqrt_lt_square; try order'.
+ rewrite <- (mul_1_r a) at 1.
+ rewrite <- mul_lt_mono_pos_l; order'.
+Qed.
+
+Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.
+Proof.
+ intros a Ha.
+ destruct (le_gt_cases a 0) as [H|H].
+ setoid_replace a with 0 by order. now rewrite sqrt_0.
+ destruct (le_gt_cases a 1) as [H'|H'].
+ rewrite <- le_succ_l, <- one_succ in H.
+ setoid_replace a with 1 by order. now rewrite sqrt_1.
+ now apply lt_le_incl, sqrt_lt_lin.
+Qed.
+
+(** Sqrt and multiplication. *)
+
+(** Due to rounding error, we don't have the usual √(a*b) = √a*√b
+    but only lower and upper bounds. *)
+
+Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
+Proof.
+ intros a b.
+ destruct (lt_ge_cases a 0) as [Ha|Ha].
+ rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg.
+ assert (Ha':=sqrt_nonneg a).
+ assert (Hb':=sqrt_nonneg b).
+ apply sqrt_le_square; try now apply mul_nonneg_nonneg.
+ rewrite mul_shuffle1.
+ apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg.
+  now apply sqrt_spec.
+  now apply sqrt_spec.
+Qed.
+
+Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b).
+Proof.
+ intros a b Ha Hb.
+ apply sqrt_lt_square.
+ now apply mul_nonneg_nonneg.
+ apply mul_nonneg_nonneg.
+ now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+ now apply lt_le_incl, lt_succ_r, sqrt_nonneg.
+ rewrite mul_shuffle1.
+ apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec.
+Qed.
+
+(** And we can't find better approximations in general.
+    - The lower bound is exact for squares
+    - Concerning the upper bound, for any c>0, take a=b=c²-1,
+      then √(a*b) = c² -1 while S √a = S √b = c
+*)
+
+(** Sqrt and successor :
+    - the sqrt function climbs by at most 1 at a time
+    - otherwise it stays at the same value
+    - the +1 steps occur for squares
+*)
+
+Lemma sqrt_succ_le : forall a, 0<=a -> √(S a) <= S (√a).
+Proof.
+ intros a Ha.
+ apply lt_succ_r.
+ apply sqrt_lt_square.
+ now apply le_le_succ_r.
+ apply le_le_succ_r, le_le_succ_r, sqrt_nonneg.
+ rewrite <- (add_1_l (S (√a))).
+ apply lt_le_trans with (1²+(S (√a))²).
+ rewrite mul_1_l, add_1_l, <- succ_lt_mono.
+ now apply sqrt_spec.
+ apply add_square_le. order'. apply le_le_succ_r, sqrt_nonneg.
+Qed.
+
+Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (√a) \/ √(S a) == √a.
+Proof.
+ intros a Ha.
+ destruct (le_gt_cases (√(S a)) (√a)) as [H|H].
+ right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order.
+ left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order.
+Qed.
+
+Lemma sqrt_eq_succ_iff_square : forall a, 0<=a ->
+ (√(S a) == S (√a) <-> exists b, 0<b /\ S a == b²).
+Proof.
+ intros a Ha. split.
+ intros EQ. exists (S (√a)).
+ split. apply lt_succ_r, sqrt_nonneg.
+ generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l.
+ assert (Ha' : 0 <= S a) by now apply le_le_succ_r.
+ generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order.
+ intros (b & Hb & H).
+ rewrite H. rewrite sqrt_square; try order.
+ symmetry.
+ rewrite <- (lt_succ_pred 0 b Hb). f_equiv.
+ rewrite <- (lt_succ_pred 0 b²) in H. apply succ_inj in H.
+ now rewrite H, sqrt_pred_square.
+ now apply mul_pos_pos.
+Qed.
+
+(** Sqrt and addition *)
+
+Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.
+Proof.
+ assert (AUX : forall a b, a<0 -> √(a+b) <= √a + √b).
+  intros a b Ha. rewrite (sqrt_neg a Ha). nzsimpl.
+  apply sqrt_le_mono.
+  rewrite <- (add_0_l b) at 2.
+  apply add_le_mono_r; order.
+ intros a b.
+ destruct (lt_ge_cases a 0) as [Ha|Ha]. now apply AUX.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+  rewrite (add_comm a), (add_comm (√a)); now apply AUX.
+ assert (Ha':=sqrt_nonneg a).
+ assert (Hb':=sqrt_nonneg b).
+ rewrite <- lt_succ_r.
+ apply sqrt_lt_square.
+  now apply add_nonneg_nonneg.
+  now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg.
+ destruct (sqrt_spec a Ha) as (_,LTa).
+ destruct (sqrt_spec b Hb) as (_,LTb).
+ revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r.
+ intros LTa LTb.
+ assert (H:=add_le_mono _ _ _ _ LTa LTb).
+ etransitivity; [eexact H|]. clear LTa LTb H.
+ rewrite <- (add_assoc _ (√a) (√a)).
+ rewrite <- (add_assoc _ (√b) (√b)).
+ rewrite add_shuffle1.
+ rewrite <- (add_assoc _ (√a + √b)).
+ rewrite (add_shuffle1 (√a) (√b)).
+ apply add_le_mono_r.
+ now apply add_square_le.
+Qed.
+
+(** convexity inequality for sqrt: sqrt of middle is above middle
+    of square roots. *)
+
+Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> √a + √b <= √(2*(a+b)).
+Proof.
+ intros a b Ha Hb.
+ assert (Ha':=sqrt_nonneg a).
+ assert (Hb':=sqrt_nonneg b).
+ apply sqrt_le_square.
+  apply mul_nonneg_nonneg. order'. now apply add_nonneg_nonneg.
+  now apply add_nonneg_nonneg.
+ transitivity (2*((√a)² + (√b)²)).
+ now apply square_add_le.
+ apply mul_le_mono_nonneg_l. order'.
+ apply add_le_mono; now apply sqrt_spec.
+Qed.
+
+End NZSqrtProp.
+
+Module Type NZSqrtUpProp
+ (Import A : NZDecOrdAxiomsSig')
+ (Import B : NZSqrt' A)
+ (Import C : NZMulOrderProp A)
+ (Import D : NZSqrtProp A B C).
+
+(** * [sqrt_up] : a square root that rounds up instead of down *)
+
+Local Notation "a ²" := (a*a) (at level 5, no associativity, format "a ²").
+
+(** For once, we define instead of axiomatizing, thanks to sqrt *)
+
+Definition sqrt_up a :=
+ match compare 0 a with
+  | Lt => S √(P a)
+  | _ => 0
+ end.
+
+Local Notation "√° a" := (sqrt_up a) (at level 6, no associativity).
+
+Lemma sqrt_up_eqn0 : forall a, a<=0 -> √°a == 0.
+Proof.
+ intros a Ha. unfold sqrt_up. case compare_spec; try order.
+Qed.
+
+Lemma sqrt_up_eqn : forall a, 0<a -> √°a == S √(P a).
+Proof.
+ intros a Ha. unfold sqrt_up. case compare_spec; try order.
+Qed.
+
+Lemma sqrt_up_spec : forall a, 0<a -> (P √°a)² < a <= (√°a)².
+Proof.
+ intros a Ha.
+ rewrite sqrt_up_eqn, pred_succ; trivial.
+ assert (Ha' := lt_succ_pred 0 a Ha).
+ rewrite <- Ha' at 3 4.
+ rewrite le_succ_l, lt_succ_r.
+ apply sqrt_spec.
+ now rewrite <- lt_succ_r, Ha'.
+Qed.
+
+(** First, [sqrt_up] is non-negative *)
+
+Lemma sqrt_up_nonneg : forall a, 0<=√°a.
+Proof.
+ intros. destruct (le_gt_cases a 0) as [Ha|Ha].
+ now rewrite sqrt_up_eqn0.
+ rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg.
+Qed.
+
+(** [sqrt_up] is a morphism *)
+
+Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up.
+Proof.
+ assert (Proper (eq==>eq==>Logic.eq) compare).
+  intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order.
+ intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx.
+Qed.
+
+(** The spec of [sqrt_up] indeed determines it *)
+
+Lemma sqrt_up_unique : forall a b, 0<b -> (P b)² < a <= b² -> √°a == b.
+Proof.
+ intros a b Hb (LEb,LTb).
+ assert (Ha : 0<a)
+  by (apply le_lt_trans with (P b)²; trivial using square_nonneg).
+ rewrite sqrt_up_eqn; trivial.
+ assert (Hb' := lt_succ_pred 0 b Hb).
+ rewrite <- Hb'. f_equiv. apply sqrt_unique.
+ rewrite <- le_succ_l, <- lt_succ_r, Hb'.
+ rewrite (lt_succ_pred 0 a Ha). now split.
+Qed.
+
+(** [sqrt_up] is exact on squares *)
+
+Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a.
+Proof.
+ intros a Ha.
+ le_elim Ha.
+ rewrite sqrt_up_eqn by (now apply mul_pos_pos).
+ rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial.
+ rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl.
+Qed.
+
+(** [sqrt_up] and successors of squares *)
+
+Lemma sqrt_up_succ_square : forall a, 0<=a -> √°(S a²) == S a.
+Proof.
+ intros a Ha.
+ rewrite sqrt_up_eqn by (now apply lt_succ_r, mul_nonneg_nonneg).
+ now rewrite pred_succ, sqrt_square.
+Qed.
+
+(** Basic constants *)
+
+Lemma sqrt_up_0 : √°0 == 0.
+Proof.
+ rewrite <- (mul_0_l 0) at 1. now apply sqrt_up_square.
+Qed.
+
+Lemma sqrt_up_1 : √°1 == 1.
+Proof.
+ rewrite <- (mul_1_l 1) at 1. apply sqrt_up_square. order'.
+Qed.
+
+Lemma sqrt_up_2 : √°2 == 2.
+Proof.
+ rewrite sqrt_up_eqn by order'.
+ now rewrite two_succ, pred_succ, sqrt_1.
+Qed.
+
+(**  Links between sqrt and [sqrt_up] *)
+
+Lemma le_sqrt_sqrt_up : forall a, √a <= √°a.
+Proof.
+ intros a. unfold sqrt_up. case compare_spec; intros H.
+ rewrite <- H, sqrt_0. order.
+ rewrite <- (lt_succ_pred 0 a H) at 1. apply sqrt_succ_le.
+ apply lt_succ_r. now rewrite (lt_succ_pred 0 a H).
+ now rewrite sqrt_neg.
+Qed.
+
+Lemma le_sqrt_up_succ_sqrt : forall a, √°a <= S (√a).
+Proof.
+ intros a. unfold sqrt_up.
+ case compare_spec; intros H; try apply le_le_succ_r, sqrt_nonneg.
+ rewrite <- succ_le_mono. apply sqrt_le_mono.
+ rewrite <- (lt_succ_pred 0 a H) at 2. apply le_succ_diag_r.
+Qed.
+
+Lemma sqrt_sqrt_up_spec : forall a, 0<=a -> (√a)² <= a <= (√°a)².
+Proof.
+ intros a H. split.
+ now apply sqrt_spec.
+ le_elim H.
+ now apply sqrt_up_spec.
+ now rewrite <-H, sqrt_up_0, mul_0_l.
+Qed.
+
+Lemma sqrt_sqrt_up_exact :
+ forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²).
+Proof.
+ intros a Ha.
+ split. intros. exists √a.
+  split. apply sqrt_nonneg.
+  generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order.
+ intros (b & Hb & Hb'). rewrite Hb'.
+ now rewrite sqrt_square, sqrt_up_square.
+Qed.
+
+(** [sqrt_up] is a monotone function (but not a strict one) *)
+
+Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases a 0) as [Ha|Ha].
+ rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg.
+ rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono.
+ apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order.
+Qed.
+
+(** No reverse result for <=, consider for instance √°3 <= √°2 *)
+
+Lemma sqrt_up_lt_cancel : forall a b, √°a < √°b -> a < b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases b 0) as [Hb|Hb].
+ rewrite (sqrt_up_eqn0 _ Hb) in H; generalize (sqrt_up_nonneg a); order.
+ destruct (le_gt_cases a 0) as [Ha|Ha]; [order|].
+ rewrite <- (lt_succ_pred 0 a Ha), <- (lt_succ_pred 0 b Hb), <- succ_lt_mono.
+ apply sqrt_lt_cancel, succ_lt_mono. now rewrite <- 2 sqrt_up_eqn.
+Qed.
+
+(** When left side is a square, we have an equivalence for < *)
+
+Lemma sqrt_up_lt_square : forall a b, 0<=a -> 0<=b -> (b² < a <-> b < √°a).
+Proof.
+ intros a b Ha Hb. split; intros H.
+ destruct (sqrt_up_spec a) as (LE,LT).
+ apply le_lt_trans with b²; trivial using square_nonneg.
+ apply square_lt_simpl_nonneg; try order. apply sqrt_up_nonneg.
+ apply sqrt_up_lt_cancel. now rewrite sqrt_up_square.
+Qed.
+
+(** When right side is a square, we have an equivalence for <= *)
+
+Lemma sqrt_up_le_square : forall a b, 0<=a -> 0<=b -> (a <= b² <-> √°a <= b).
+Proof.
+ intros a b Ha Hb. split; intros H.
+ rewrite <- (sqrt_up_square b Hb).
+ now apply sqrt_up_le_mono.
+ apply square_le_mono_nonneg in H; [|now apply sqrt_up_nonneg].
+ transitivity (√°a)²; trivial. now apply sqrt_sqrt_up_spec.
+Qed.
+
+Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a.
+Proof.
+ intros a. split; intros Ha. apply sqrt_up_lt_cancel. now rewrite sqrt_up_0.
+ rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono.
+ now rewrite one_succ, le_succ_l.
+Qed.
+
+Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a.
+Proof.
+ intros a Ha.
+ rewrite sqrt_up_eqn by order'.
+ assert (Ha' := lt_succ_pred 2 a Ha).
+ rewrite <- Ha' at 2. rewrite <- succ_lt_mono.
+ apply sqrt_lt_lin. rewrite succ_lt_mono. now rewrite Ha', <- two_succ.
+Qed.
+
+Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a.
+Proof.
+ intros a Ha.
+ le_elim Ha.
+ rewrite sqrt_up_eqn; trivial. apply le_succ_l.
+ apply le_lt_trans with (P a). apply sqrt_le_lin.
+ now rewrite <- lt_succ_r, (lt_succ_pred 0).
+ rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r.
+ now rewrite <- Ha, sqrt_up_0.
+Qed.
+
+(** [sqrt_up] and multiplication. *)
+
+(** Due to rounding error, we don't have the usual [√(a*b) = √a*√b]
+    but only lower and upper bounds. *)
+
+Lemma sqrt_up_mul_above : forall a b, 0<=a -> 0<=b -> √°(a*b) <= √°a * √°b.
+Proof.
+ intros a b Ha Hb.
+ apply sqrt_up_le_square.
+ now apply mul_nonneg_nonneg.
+ apply mul_nonneg_nonneg; apply sqrt_up_nonneg.
+ rewrite mul_shuffle1.
+ apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec.
+Qed.
+
+Lemma sqrt_up_mul_below : forall a b, 0<a -> 0<b -> (P √°a)*(P √°b) < √°(a*b).
+Proof.
+ intros a b Ha Hb.
+ apply sqrt_up_lt_square.
+ apply mul_nonneg_nonneg; order.
+ apply mul_nonneg_nonneg; apply lt_succ_r.
+ rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
+ rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos.
+ rewrite mul_shuffle1.
+ apply mul_lt_mono_nonneg; trivial using square_nonneg;
+  now apply sqrt_up_spec.
+Qed.
+
+(** And we can't find better approximations in general.
+    - The upper bound is exact for squares
+    - Concerning the lower bound, for any c>0, take [a=b=c²+1],
+      then [√°(a*b) = c²+1] while [P √°a = P √°b = c]
+*)
+
+(** [sqrt_up] and successor :
+    - the [sqrt_up] function climbs by at most 1 at a time
+    - otherwise it stays at the same value
+    - the +1 steps occur after squares
+*)
+
+Lemma sqrt_up_succ_le : forall a, 0<=a -> √°(S a) <= S (√°a).
+Proof.
+ intros a Ha.
+ apply sqrt_up_le_square.
+ now apply le_le_succ_r.
+ apply le_le_succ_r, sqrt_up_nonneg.
+ rewrite <- (add_1_l (√°a)).
+ apply le_trans with (1²+(√°a)²).
+ rewrite mul_1_l, add_1_l, <- succ_le_mono.
+ now apply sqrt_sqrt_up_spec.
+ apply add_square_le. order'. apply sqrt_up_nonneg.
+Qed.
+
+Lemma sqrt_up_succ_or : forall a, 0<=a -> √°(S a) == S (√°a) \/ √°(S a) == √°a.
+Proof.
+ intros a Ha.
+ destruct (le_gt_cases (√°(S a)) (√°a)) as [H|H].
+ right. generalize (sqrt_up_le_mono _ _ (le_succ_diag_r a)); order.
+ left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order.
+Qed.
+
+Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a ->
+ (√°(S a) == S (√°a) <-> exists b, 0<=b /\ a == b²).
+Proof.
+ intros a Ha. split.
+ intros EQ.
+ le_elim Ha.
+ exists (√°a). split. apply sqrt_up_nonneg.
+ generalize (proj2 (sqrt_up_spec a Ha)).
+ assert (Ha' : 0 < S a) by (apply lt_succ_r; order').
+ generalize (proj1 (sqrt_up_spec (S a) Ha')).
+ rewrite EQ, pred_succ, lt_succ_r. order.
+ exists 0. nzsimpl. now split.
+ intros (b & Hb & H).
+ now rewrite H, sqrt_up_succ_square, sqrt_up_square.
+Qed.
+
+(** [sqrt_up] and addition *)
+
+Lemma sqrt_up_add_le : forall a b, √°(a+b) <= √°a + √°b.
+Proof.
+ assert (AUX : forall a b, a<=0 -> √°(a+b) <= √°a + √°b).
+  intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl.
+  apply sqrt_up_le_mono.
+  rewrite <- (add_0_l b) at 2.
+  apply add_le_mono_r; order.
+ intros a b.
+ destruct (le_gt_cases a 0) as [Ha|Ha]. now apply AUX.
+ destruct (le_gt_cases b 0) as [Hb|Hb].
+  rewrite (add_comm a), (add_comm (√°a)); now apply AUX.
+ rewrite 2 sqrt_up_eqn; trivial.
+ nzsimpl. rewrite <- succ_le_mono.
+ transitivity (√(P a) + √b).
+ rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le.
+ apply add_le_mono_l.
+ apply le_sqrt_sqrt_up.
+ now apply add_pos_pos.
+Qed.
+
+(** Convexity-like inequality for [sqrt_up]: [sqrt_up] of middle is above middle
+    of square roots. We cannot say more, for instance take a=b=2, then
+    2+2 <= S 3 *)
+
+Lemma add_sqrt_up_le : forall a b, 0<=a -> 0<=b -> √°a + √°b <= S √°(2*(a+b)).
+Proof.
+ intros a b Ha Hb.
+ le_elim Ha.
+ le_elim Hb.
+ rewrite 3 sqrt_up_eqn; trivial.
+ nzsimpl. rewrite <- 2 succ_le_mono.
+ etransitivity; [eapply add_sqrt_le|].
+ apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha).
+ apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb).
+ apply sqrt_le_mono.
+ apply lt_succ_r. rewrite (lt_succ_pred 0).
+ apply mul_lt_mono_pos_l. order'.
+ apply add_lt_mono.
+ apply le_succ_l. now rewrite (lt_succ_pred 0).
+ apply le_succ_l. now rewrite (lt_succ_pred 0).
+ apply mul_pos_pos. order'. now apply add_pos_pos.
+ apply mul_pos_pos. order'. now apply add_pos_pos.
+ rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono.
+ rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'.
+ rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono.
+ rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'.
+Qed.
+
+End NZSqrtUpProp.