8 files changed, 22 insertions, 43 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
index b73410256..05b8ede94 100644
--- a/theories/Numbers/Integer/Axioms/ZAxioms.v
+++ b/theories/Numbers/Integer/Axioms/ZAxioms.v
@@ -1,5 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
+Require Export ZDomain.
 
 Module Type IntSignature.
 Declare Module Export DomainModule : DomainSignature.
@@ -25,7 +24,6 @@ Axiom induction :
 
 End IntSignature.
 
-
 Module IntProperties (Export IntModule : IntSignature).
 Module Export DomainPropertiesModule := DomainProperties DomainModule.
 Open Local Scope ZScope.
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
index b48684ba8..1a29eddf2 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -1,4 +1,4 @@
-Require Import NumPrelude.
+Require Export NumPrelude.
 
 Module Type DomainSignature.
 
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v
index 3bf4d61f5..803bfe43b 100644
--- a/theories/Numbers/Integer/Axioms/ZOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZOrder.v
@@ -1,6 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
-Require Import ZAxioms.
+Require Export ZAxioms.
 
 Module Type OrderSignature.
 Declare Module Export IntModule : IntSignature.
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v
index f455400b7..484607094 100644
--- a/theories/Numbers/Integer/Axioms/ZPlus.v
+++ b/theories/Numbers/Integer/Axioms/ZPlus.v
@@ -1,6 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
-Require Import ZAxioms.
+Require Export ZAxioms.
 
 Module Type PlusSignature.
 Declare Module Export IntModule : IntSignature.
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
index 4f677355b..dd311b49a 100644
--- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
@@ -1,8 +1,8 @@
-Require Import ZOrder.
-Require Import ZPlus.
+Require Export ZOrder.
+Require Export ZPlus.
 
-Module PlusOrderProperties (Export PlusModule : PlusSignature)
-                           (Export OrderModule : OrderSignature with
+Module PlusOrderProperties (PlusModule : PlusSignature)
+                           (OrderModule : OrderSignature with
                              Module IntModule := PlusModule.IntModule).
 (* Warning: Notation _ == _ was already used in scope ZScope !!! *)
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
index ff0de6196..052dcf66f 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -1,7 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
-Require Import ZAxioms.
-Require Import ZPlus.
+Require Export ZPlus.
 
 Module Type TimesSignature.
 Declare Module Export PlusModule : PlusSignature.
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
index 460a13bf4..a72636a42 100644
--- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
@@ -1,12 +1,9 @@
-Require Import ZPlus.
-Require Import ZTimes.
-Require Import ZOrder.
-Require Import ZPlusOrder.
+Require Export ZTimes.
+Require Export ZPlusOrder.
 
-Module TimesOrderProperties (Export TimesModule : TimesSignature)
-                            (Export OrderModule : OrderSignature with
+Module TimesOrderProperties (TimesModule : TimesSignature)
+                            (OrderModule : OrderSignature with
                               Module IntModule := TimesModule.PlusModule.IntModule).
-
 Module Export TimesPropertiesModule := TimesProperties TimesModule.
 Module Export PlusOrderPropertiesModule :=
   PlusOrderProperties TimesModule.PlusModule OrderModule.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 02f73f4d1..2ca4bc5d8 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,21 +1,12 @@
-Require Import NDomain.
-Require Import NAxioms.
-Require Import NPlus.
-Require Import NTimes.
-Require Import NLt.
-Require Import NPlusLt.
-Require Import NTimesLt.
-
-Require Import ZDomain.
-Require Import ZAxioms.
-Require Import ZPlus.
-Require Import ZTimes.
-Require Import ZOrder.
-Require Import ZPlusOrder.
-Require Import ZTimesOrder.
-
-Module NatPairsDomain (NPlusModule : NPlus.PlusSignature) <:
-  ZDomain.DomainSignature.
+Require Export NTimesLt.
+Require Export ZTimesOrder.
+
+Module NatPairsDomain (Export NPlusModule : NPlus.PlusSignature) :
+  ZDomain.DomainSignature
+  with Definition Z := (N * N)%type.
+  with Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat.
+  with Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat.
+
 Module Export NPlusPropertiesModule := NPlus.PlusProperties NPlusModule.
 
 Definition Z : Set := (N * N)%type.