3 files changed, 21 insertions, 10 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 8973df3589..446fd7eb80 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -9,11 +9,22 @@
 Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor
  ZGcd ZLcm NZLog NZSqrt ZBits.
 
-(** This functor summarizes all known facts about Z. *)
+(** The two following functors summarize all known facts about N.
 
-Module Type ZProp (Z:ZAxiomsSig) :=
- ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
- <+ NZSqrtProp Z Z <+ NZSqrtUpProp Z Z
- <+ NZLog2Prop Z Z Z <+ NZLog2UpProp Z Z Z
- <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z
- <+ ZBitsProp Z.
+    - [ZBasicProp] provides properties of basic functions:
+      + - * min max <= <
+
+    - [ZExtraProp] provides properties of advanced functions:
+      pow, sqrt, log2, div, gcd, and bitwise functions.
+
+    If necessary, the earlier all-in-one functor [ZProp]
+    could be re-obtained via [ZBasicProp <+ ZExtraProp] *)
+
+Module Type ZBasicProp (Z:ZAxiomsMiniSig) := ZMaxMinProp Z.
+
+Module Type ZExtraProp (Z:ZAxiomsSig)(P:ZBasicProp Z) :=
+ ZSgnAbsProp Z P <+ ZParityProp Z P <+ ZPowProp Z P
+ <+ NZSqrtProp Z Z P <+ NZSqrtUpProp Z Z P
+ <+ NZLog2Prop Z Z Z P <+ NZLog2UpProp Z Z Z P
+ <+ ZDivProp Z P <+ ZQuotProp Z P <+ ZGcdProp Z P <+ ZLcmProp Z P
+ <+ ZBitsProp Z P.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index eca97ace9a..c1c78d9111 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -29,7 +29,7 @@ Delimit Scope bigZ_scope with bigZ.
 Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
  ZMake.Make BigN
  <+ ZTypeIsZAxioms
- <+ ZProp [no inline]
+ <+ ZBasicProp [no inline] <+ ZExtraProp [no inline]
  <+ HasEqBool2Dec [no inline]
  <+ MinMaxLogicalProperties [no inline]
  <+ MinMaxDecProperties [no inline].
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index b5e1fa5b0e..11eb6e4d0d 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -332,9 +332,9 @@ and get their properties *)
 
 (* The following lines increase the compilation time at least twice *)
 (*
-Require Import NPeano.
+Require PeanoNat.
 
-Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod.
+Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod PeanoNat.Nat.
 Module Export ZPairsPropMod := ZPropFunct ZPairsPeanoAxiomsMod.
 
 Eval compute in (3, 5) * (4, 6).