1 files changed, 28 insertions, 19 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
index 5f592dbcb9..683b86ec6e 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
@@ -1,5 +1,5 @@
-Require Export NTimesOrder.
-Require Export ZTimesOrder.
+Require Import NPlus.
+Require Export ZAxioms.
 
 Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
 (*  with Definition Z :=
@@ -11,7 +11,7 @@ Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
     fun p1 p2  =>
       NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
 
-Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule.
 Open Local Scope NatScope.
 
 Definition Z : Set := (N * N)%type.
@@ -28,26 +28,35 @@ Proof.
 intros x y; unfold E, e; apply E_equiv_e.
 Qed.
 
-Theorem E_equiv : equiv Z E.
+Theorem ZE_refl : reflexive Z E.
+Proof.
+unfold reflexive, E; reflexivity.
+Qed.
+
+Theorem ZE_symm : symmetric Z E.
 Proof.
-split; [| split]; unfold reflexive, symmetric, transitive, E.
-(* reflexivity *)
-now intro.
-(* transitivity *)
-intros x y z H1 H2.
+unfold symmetric, E; now symmetry.
+Qed.
+
+Theorem ZE_trans : transitive Z E.
+Proof.
+unfold transitive, E. intros x y z H1 H2.
 apply plus_cancel_l with (p := fst y + snd y).
 rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)).
 rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)).
 rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)).
 rewrite (plus_comm (snd y) (fst z)). now apply plus_wd.
-(* symmetry *)
-now intros.
 Qed.
 
-Add Relation Z E                                                                                 
- reflexivity proved by (proj1 E_equiv)                                                           
- symmetry proved by (proj2 (proj2 E_equiv))                                                      
- transitivity proved by (proj1 (proj2 E_equiv))                                                  
+Theorem E_equiv : equiv Z E.
+Proof.
+unfold equiv; split; [apply ZE_refl | split; [apply ZE_trans | apply ZE_symm]].
+Qed.
+
+Add Relation Z E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
 Add Morphism (@pair N N)
@@ -78,25 +87,25 @@ Notation "0" := O : IntScope.
 Add Morphism S with signature E ==> E as S_wd.
 Proof.
 unfold S, E; intros n m H; simpl.
-do 2 rewrite plus_Sn_m; now rewrite H.
+do 2 rewrite plus_S_l; now rewrite H.
 Qed.
 
 Add Morphism P with signature E ==> E as P_wd.
 Proof.
 unfold P, E; intros n m H; simpl.
-do 2 rewrite plus_n_Sm; now rewrite H.
+do 2 rewrite plus_S_r; now rewrite H.
 Qed.
 
 Theorem S_inj : forall x y : Z, S x == S y -> x == y.
 Proof.
 unfold S, E; simpl; intros x y H.
-do 2 rewrite plus_Sn_m in H. now apply S_inj in H.
+do 2 rewrite plus_S_l in H. now apply S_inj in H.
 Qed.
 
 Theorem S_P : forall x : Z, S (P x) == x.
 Proof.
 intro x; unfold S, P, E; simpl.
-rewrite plus_Sn_m; now rewrite plus_n_Sm.
+rewrite plus_S_l; now rewrite plus_S_r.
 Qed.
 
 Section Induction.