Simplification of Numbers, mainly thanks to Include

 - No more nesting of Module and Module Type, we rather use Include.
 - Instead of in-name-qualification like NZeq, we use uniform
   short names + modular qualification like N.eq when necessary.
 - Many simplification of proofs, by some autorewrite for instance
 - In NZOrder, we instantiate an "order" tactic.
 - Some requirements in NZAxioms were superfluous: compatibility
   of le, min and max could be derived from the rest.
 - NMul removed, since it was containing only an ad-hoc result for
   ZNatPairs, that we've inlined in the proof of mul_wd there.
 - Zdomain removed (was already not compiled), idea of a module
   with eq and eqb reused in DecidableType.BooleanEqualityType.
 - ZBinDefs don't contain any definition now, migrate it to ZBinary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 815 insertions, 1693 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index daa7c530b9..26ba0a8d40 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -12,334 +12,283 @@
 
 Require Export ZBase.
 
-Module ZAddPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZBasePropMod := ZBasePropFunct ZAxiomsMod.
-Open Local Scope IntScope.
+Module ZAddPropFunct (Import Z : ZAxiomsSig).
+Include ZBasePropFunct Z.
+Local Open Scope NumScope.
 
-Theorem Zadd_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 + m1 == n2 + m2.
-Proof NZadd_wd.
+(** Theorems that are either not valid on N or have different proofs
+    on N and Z *)
 
-Theorem Zadd_0_l : forall n : Z, 0 + n == n.
-Proof NZadd_0_l.
-
-Theorem Zadd_succ_l : forall n m : Z, (S n) + m == S (n + m).
-Proof NZadd_succ_l.
-
-Theorem Zsub_0_r : forall n : Z, n - 0 == n.
-Proof NZsub_0_r.
-
-Theorem Zsub_succ_r : forall n m : Z, n - (S m) == P (n - m).
-Proof NZsub_succ_r.
-
-Theorem Zopp_0 : - 0 == 0.
-Proof Zopp_0.
-
-Theorem Zopp_succ : forall n : Z, - (S n) == P (- n).
-Proof Zopp_succ.
-
-(* Theorems that are valid for both natural numbers and integers *)
-
-Theorem Zadd_0_r : forall n : Z, n + 0 == n.
-Proof NZadd_0_r.
-
-Theorem Zadd_succ_r : forall n m : Z, n + S m == S (n + m).
-Proof NZadd_succ_r.
-
-Theorem Zadd_comm : forall n m : Z, n + m == m + n.
-Proof NZadd_comm.
-
-Theorem Zadd_assoc : forall n m p : Z, n + (m + p) == (n + m) + p.
-Proof NZadd_assoc.
-
-Theorem Zadd_shuffle1 : forall n m p q : Z, (n + m) + (p + q) == (n + p) + (m + q).
-Proof NZadd_shuffle1.
-
-Theorem Zadd_shuffle2 : forall n m p q : Z, (n + m) + (p + q) == (n + q) + (m + p).
-Proof NZadd_shuffle2.
-
-Theorem Zadd_1_l : forall n : Z, 1 + n == S n.
-Proof NZadd_1_l.
-
-Theorem Zadd_1_r : forall n : Z, n + 1 == S n.
-Proof NZadd_1_r.
-
-Theorem Zadd_cancel_l : forall n m p : Z, p + n == p + m <-> n == m.
-Proof NZadd_cancel_l.
-
-Theorem Zadd_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
-Proof NZadd_cancel_r.
-
-(* Theorems that are either not valid on N or have different proofs on N and Z *)
-
-Theorem Zadd_pred_l : forall n m : Z, P n + m == P (n + m).
+Theorem add_pred_l : forall n m, P n + m == P (n + m).
 Proof.
 intros n m.
-rewrite <- (Zsucc_pred n) at 2.
-rewrite Zadd_succ_l. now rewrite Zpred_succ.
+rewrite <- (succ_pred n) at 2.
+rewrite add_succ_l. now rewrite pred_succ.
 Qed.
 
-Theorem Zadd_pred_r : forall n m : Z, n + P m == P (n + m).
+Theorem add_pred_r : forall n m, n + P m == P (n + m).
 Proof.
-intros n m; rewrite (Zadd_comm n (P m)), (Zadd_comm n m);
-apply Zadd_pred_l.
+intros n m; rewrite (add_comm n (P m)), (add_comm n m);
+apply add_pred_l.
 Qed.
 
-Theorem Zadd_opp_r : forall n m : Z, n + (- m) == n - m.
+Theorem add_opp_r : forall n m, n + (- m) == n - m.
 Proof.
-NZinduct m.
-rewrite Zopp_0; rewrite Zsub_0_r; now rewrite Zadd_0_r.
-intro m. rewrite Zopp_succ, Zsub_succ_r, Zadd_pred_r; now rewrite Zpred_inj_wd.
+nzinduct m.
+rewrite opp_0; rewrite sub_0_r; now rewrite add_0_r.
+intro m. rewrite opp_succ, sub_succ_r, add_pred_r; now rewrite pred_inj_wd.
 Qed.
 
-Theorem Zsub_0_l : forall n : Z, 0 - n == - n.
+Theorem sub_0_l : forall n, 0 - n == - n.
 Proof.
-intro n; rewrite <- Zadd_opp_r; now rewrite Zadd_0_l.
+intro n; rewrite <- add_opp_r; now rewrite add_0_l.
 Qed.
 
-Theorem Zsub_succ_l : forall n m : Z, S n - m == S (n - m).
+Theorem sub_succ_l : forall n m, S n - m == S (n - m).
 Proof.
-intros n m; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_succ_l.
+intros n m; do 2 rewrite <- add_opp_r; now rewrite add_succ_l.
 Qed.
 
-Theorem Zsub_pred_l : forall n m : Z, P n - m == P (n - m).
+Theorem sub_pred_l : forall n m, P n - m == P (n - m).
 Proof.
-intros n m. rewrite <- (Zsucc_pred n) at 2.
-rewrite Zsub_succ_l; now rewrite Zpred_succ.
+intros n m. rewrite <- (succ_pred n) at 2.
+rewrite sub_succ_l; now rewrite pred_succ.
 Qed.
 
-Theorem Zsub_pred_r : forall n m : Z, n - (P m) == S (n - m).
+Theorem sub_pred_r : forall n m, n - (P m) == S (n - m).
 Proof.
-intros n m. rewrite <- (Zsucc_pred m) at 2.
-rewrite Zsub_succ_r; now rewrite Zsucc_pred.
+intros n m. rewrite <- (succ_pred m) at 2.
+rewrite sub_succ_r; now rewrite succ_pred.
 Qed.
 
-Theorem Zopp_pred : forall n : Z, - (P n) == S (- n).
+Theorem opp_pred : forall n, - (P n) == S (- n).
 Proof.
-intro n. rewrite <- (Zsucc_pred n) at 2.
-rewrite Zopp_succ. now rewrite Zsucc_pred.
+intro n. rewrite <- (succ_pred n) at 2.
+rewrite opp_succ. now rewrite succ_pred.
 Qed.
 
-Theorem Zsub_diag : forall n : Z, n - n == 0.
+Theorem sub_diag : forall n, n - n == 0.
 Proof.
-NZinduct n.
-now rewrite Zsub_0_r.
-intro n. rewrite Zsub_succ_r, Zsub_succ_l; now rewrite Zpred_succ.
+nzinduct n.
+now rewrite sub_0_r.
+intro n. rewrite sub_succ_r, sub_succ_l; now rewrite pred_succ.
 Qed.
 
-Theorem Zadd_opp_diag_l : forall n : Z, - n + n == 0.
+Theorem add_opp_diag_l : forall n, - n + n == 0.
 Proof.
-intro n; now rewrite Zadd_comm, Zadd_opp_r, Zsub_diag.
+intro n; now rewrite add_comm, add_opp_r, sub_diag.
 Qed.
 
-Theorem Zadd_opp_diag_r : forall n : Z, n + (- n) == 0.
+Theorem add_opp_diag_r : forall n, n + (- n) == 0.
 Proof.
-intro n; rewrite Zadd_comm; apply Zadd_opp_diag_l.
+intro n; rewrite add_comm; apply add_opp_diag_l.
 Qed.
 
-Theorem Zadd_opp_l : forall n m : Z, - m + n == n - m.
+Theorem add_opp_l : forall n m, - m + n == n - m.
 Proof.
-intros n m; rewrite <- Zadd_opp_r; now rewrite Zadd_comm.
+intros n m; rewrite <- add_opp_r; now rewrite add_comm.
 Qed.
 
-Theorem Zadd_sub_assoc : forall n m p : Z, n + (m - p) == (n + m) - p.
+Theorem add_sub_assoc : forall n m p, n + (m - p) == (n + m) - p.
 Proof.
-intros n m p; do 2 rewrite <- Zadd_opp_r; now rewrite Zadd_assoc.
+intros n m p; do 2 rewrite <- add_opp_r; now rewrite add_assoc.
 Qed.
 
-Theorem Zopp_involutive : forall n : Z, - (- n) == n.
+Theorem opp_involutive : forall n, - (- n) == n.
 Proof.
-NZinduct n.
-now do 2 rewrite Zopp_0.
-intro n. rewrite Zopp_succ, Zopp_pred; now rewrite Zsucc_inj_wd.
+nzinduct n.
+now do 2 rewrite opp_0.
+intro n. rewrite opp_succ, opp_pred; now rewrite succ_inj_wd.
 Qed.
 
-Theorem Zopp_add_distr : forall n m : Z, - (n + m) == - n + (- m).
+Theorem opp_add_distr : forall n m, - (n + m) == - n + (- m).
 Proof.
-intros n m; NZinduct n.
-rewrite Zopp_0; now do 2 rewrite Zadd_0_l.
-intro n. rewrite Zadd_succ_l; do 2 rewrite Zopp_succ; rewrite Zadd_pred_l.
-now rewrite Zpred_inj_wd.
+intros n m; nzinduct n.
+rewrite opp_0; now do 2 rewrite add_0_l.
+intro n. rewrite add_succ_l; do 2 rewrite opp_succ; rewrite add_pred_l.
+now rewrite pred_inj_wd.
 Qed.
 
-Theorem Zopp_sub_distr : forall n m : Z, - (n - m) == - n + m.
+Theorem opp_sub_distr : forall n m, - (n - m) == - n + m.
 Proof.
-intros n m; rewrite <- Zadd_opp_r, Zopp_add_distr.
-now rewrite Zopp_involutive.
+intros n m; rewrite <- add_opp_r, opp_add_distr.
+now rewrite opp_involutive.
 Qed.
 
-Theorem Zopp_inj : forall n m : Z, - n == - m -> n == m.
+Theorem opp_inj : forall n m, - n == - m -> n == m.
 Proof.
-intros n m H. apply Zopp_wd in H. now do 2 rewrite Zopp_involutive in H.
+intros n m H. apply opp_wd in H. now do 2 rewrite opp_involutive in H.
 Qed.
 
-Theorem Zopp_inj_wd : forall n m : Z, - n == - m <-> n == m.
+Theorem opp_inj_wd : forall n m, - n == - m <-> n == m.
 Proof.
-intros n m; split; [apply Zopp_inj | apply Zopp_wd].
+intros n m; split; [apply opp_inj | apply opp_wd].
 Qed.
 
-Theorem Zeq_opp_l : forall n m : Z, - n == m <-> n == - m.
+Theorem eq_opp_l : forall n m, - n == m <-> n == - m.
 Proof.
-intros n m. now rewrite <- (Zopp_inj_wd (- n) m), Zopp_involutive.
+intros n m. now rewrite <- (opp_inj_wd (- n) m), opp_involutive.
 Qed.
 
-Theorem Zeq_opp_r : forall n m : Z, n == - m <-> - n == m.
+Theorem eq_opp_r : forall n m, n == - m <-> - n == m.
 Proof.
-symmetry; apply Zeq_opp_l.
+symmetry; apply eq_opp_l.
 Qed.
 
-Theorem Zsub_add_distr : forall n m p : Z, n - (m + p) == (n - m) - p.
+Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
 Proof.
-intros n m p; rewrite <- Zadd_opp_r, Zopp_add_distr, Zadd_assoc.
-now do 2 rewrite Zadd_opp_r.
+intros n m p; rewrite <- add_opp_r, opp_add_distr, add_assoc.
+now do 2 rewrite add_opp_r.
 Qed.
 
-Theorem Zsub_sub_distr : forall n m p : Z, n - (m - p) == (n - m) + p.
+Theorem sub_sub_distr : forall n m p, n - (m - p) == (n - m) + p.
 Proof.
-intros n m p; rewrite <- Zadd_opp_r, Zopp_sub_distr, Zadd_assoc.
-now rewrite Zadd_opp_r.
+intros n m p; rewrite <- add_opp_r, opp_sub_distr, add_assoc.
+now rewrite add_opp_r.
 Qed.
 
-Theorem sub_opp_l : forall n m : Z, - n - m == - m - n.
+Theorem sub_opp_l : forall n m, - n - m == - m - n.
 Proof.
-intros n m. do 2 rewrite <- Zadd_opp_r. now rewrite Zadd_comm.
+intros n m. do 2 rewrite <- add_opp_r. now rewrite add_comm.
 Qed.
 
-Theorem Zsub_opp_r : forall n m : Z, n - (- m) == n + m.
+Theorem sub_opp_r : forall n m, n - (- m) == n + m.
 Proof.
-intros n m; rewrite <- Zadd_opp_r; now rewrite Zopp_involutive.
+intros n m; rewrite <- add_opp_r; now rewrite opp_involutive.
 Qed.
 
-Theorem Zadd_sub_swap : forall n m p : Z, n + m - p == n - p + m.
+Theorem add_sub_swap : forall n m p, n + m - p == n - p + m.
 Proof.
-intros n m p. rewrite <- Zadd_sub_assoc, <- (Zadd_opp_r n p), <- Zadd_assoc.
-now rewrite Zadd_opp_l.
+intros n m p. rewrite <- add_sub_assoc, <- (add_opp_r n p), <- add_assoc.
+now rewrite add_opp_l.
 Qed.
 
-Theorem Zsub_cancel_l : forall n m p : Z, n - m == n - p <-> m == p.
+Theorem sub_cancel_l : forall n m p, n - m == n - p <-> m == p.
 Proof.
-intros n m p. rewrite <- (Zadd_cancel_l (n - m) (n - p) (- n)).
-do 2 rewrite Zadd_sub_assoc. rewrite Zadd_opp_diag_l; do 2 rewrite Zsub_0_l.
-apply Zopp_inj_wd.
+intros n m p. rewrite <- (add_cancel_l (n - m) (n - p) (- n)).
+do 2 rewrite add_sub_assoc. rewrite add_opp_diag_l; do 2 rewrite sub_0_l.
+apply opp_inj_wd.
 Qed.
 
-Theorem Zsub_cancel_r : forall n m p : Z, n - p == m - p <-> n == m.
+Theorem sub_cancel_r : forall n m p, n - p == m - p <-> n == m.
 Proof.
 intros n m p.
-stepl (n - p + p == m - p + p) by apply Zadd_cancel_r.
-now do 2 rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r.
+stepl (n - p + p == m - p + p) by apply add_cancel_r.
+now do 2 rewrite <- sub_sub_distr, sub_diag, sub_0_r.
 Qed.
 
-(* The next several theorems are devoted to moving terms from one side of
-an equation to the other. The name contains the operation in the original
-equation (add or sub) and the indication whether the left or right term
-is moved. *)
+(** The next several theorems are devoted to moving terms from one
+    side of an equation to the other. The name contains the operation
+    in the original equation ([add] or [sub]) and the indication
+    whether the left or right term is moved. *)
 
-Theorem Zadd_move_l : forall n m p : Z, n + m == p <-> m == p - n.
+Theorem add_move_l : forall n m p, n + m == p <-> m == p - n.
 Proof.
 intros n m p.
-stepl (n + m - n == p - n) by apply Zsub_cancel_r.
-now rewrite Zadd_comm, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
+stepl (n + m - n == p - n) by apply sub_cancel_r.
+now rewrite add_comm, <- add_sub_assoc, sub_diag, add_0_r.
 Qed.
 
-Theorem Zadd_move_r : forall n m p : Z, n + m == p <-> n == p - m.
+Theorem add_move_r : forall n m p, n + m == p <-> n == p - m.
 Proof.
-intros n m p; rewrite Zadd_comm; now apply Zadd_move_l.
+intros n m p; rewrite add_comm; now apply add_move_l.
 Qed.
 
-(* The two theorems above do not allow rewriting subformulas of the form
-n - m == p to n == p + m since subtraction is in the right-hand side of
-the equation. Hence the following two theorems. *)
+(** The two theorems above do not allow rewriting subformulas of the
+    form [n - m == p] to [n == p + m] since subtraction is in the
+    right-hand side of the equation. Hence the following two
+    theorems. *)
 
-Theorem Zsub_move_l : forall n m p : Z, n - m == p <-> - m == p - n.
+Theorem sub_move_l : forall n m p, n - m == p <-> - m == p - n.
 Proof.
-intros n m p; rewrite <- (Zadd_opp_r n m); apply Zadd_move_l.
+intros n m p; rewrite <- (add_opp_r n m); apply add_move_l.
 Qed.
 
-Theorem Zsub_move_r : forall n m p : Z, n - m == p <-> n == p + m.
+Theorem sub_move_r : forall n m p, n - m == p <-> n == p + m.
 Proof.
-intros n m p; rewrite <- (Zadd_opp_r n m). now rewrite Zadd_move_r, Zsub_opp_r.
+intros n m p; rewrite <- (add_opp_r n m). now rewrite add_move_r, sub_opp_r.
 Qed.
 
-Theorem Zadd_move_0_l : forall n m : Z, n + m == 0 <-> m == - n.
+Theorem add_move_0_l : forall n m, n + m == 0 <-> m == - n.
 Proof.
-intros n m; now rewrite Zadd_move_l, Zsub_0_l.
+intros n m; now rewrite add_move_l, sub_0_l.
 Qed.
 
-Theorem Zadd_move_0_r : forall n m : Z, n + m == 0 <-> n == - m.
+Theorem add_move_0_r : forall n m, n + m == 0 <-> n == - m.
 Proof.
-intros n m; now rewrite Zadd_move_r, Zsub_0_l.
+intros n m; now rewrite add_move_r, sub_0_l.
 Qed.
 
-Theorem Zsub_move_0_l : forall n m : Z, n - m == 0 <-> - m == - n.
+Theorem sub_move_0_l : forall n m, n - m == 0 <-> - m == - n.
 Proof.
-intros n m. now rewrite Zsub_move_l, Zsub_0_l.
+intros n m. now rewrite sub_move_l, sub_0_l.
 Qed.
 
-Theorem Zsub_move_0_r : forall n m : Z, n - m == 0 <-> n == m.
+Theorem sub_move_0_r : forall n m, n - m == 0 <-> n == m.
 Proof.
-intros n m. now rewrite Zsub_move_r, Zadd_0_l.
+intros n m. now rewrite sub_move_r, add_0_l.
 Qed.
 
-(* The following section is devoted to cancellation of like terms. The name
-includes the first operator and the position of the term being canceled. *)
+(** The following section is devoted to cancellation of like
+    terms. The name includes the first operator and the position of
+    the term being canceled. *)
 
-Theorem Zadd_simpl_l : forall n m : Z, n + m - n == m.
+Theorem add_simpl_l : forall n m, n + m - n == m.
 Proof.
-intros; now rewrite Zadd_sub_swap, Zsub_diag, Zadd_0_l.
+intros; now rewrite add_sub_swap, sub_diag, add_0_l.
 Qed.
 
-Theorem Zadd_simpl_r : forall n m : Z, n + m - m == n.
+Theorem add_simpl_r : forall n m, n + m - m == n.
 Proof.
-intros; now rewrite <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
+intros; now rewrite <- add_sub_assoc, sub_diag, add_0_r.
 Qed.
 
-Theorem Zsub_simpl_l : forall n m : Z, - n - m + n == - m.
+Theorem sub_simpl_l : forall n m, - n - m + n == - m.
 Proof.
-intros; now rewrite <- Zadd_sub_swap, Zadd_opp_diag_l, Zsub_0_l.
+intros; now rewrite <- add_sub_swap, add_opp_diag_l, sub_0_l.
 Qed.
 
-Theorem Zsub_simpl_r : forall n m : Z, n - m + m == n.
+Theorem sub_simpl_r : forall n m, n - m + m == n.
 Proof.
-intros; now rewrite <- Zsub_sub_distr, Zsub_diag, Zsub_0_r.
+intros; now rewrite <- sub_sub_distr, sub_diag, sub_0_r.
 Qed.
 
-(* Now we have two sums or differences; the name includes the two operators
-and the position of the terms being canceled *)
+(** Now we have two sums or differences; the name includes the two
+    operators and the position of the terms being canceled *)
 
-Theorem Zadd_add_simpl_l_l : forall n m p : Z, (n + m) - (n + p) == m - p.
+Theorem add_add_simpl_l_l : forall n m p, (n + m) - (n + p) == m - p.
 Proof.
-intros n m p. now rewrite (Zadd_comm n m), <- Zadd_sub_assoc,
-Zsub_add_distr, Zsub_diag, Zsub_0_l, Zadd_opp_r.
+intros n m p. now rewrite (add_comm n m), <- add_sub_assoc,
+sub_add_distr, sub_diag, sub_0_l, add_opp_r.
 Qed.
 
-Theorem Zadd_add_simpl_l_r : forall n m p : Z, (n + m) - (p + n) == m - p.
+Theorem add_add_simpl_l_r : forall n m p, (n + m) - (p + n) == m - p.
 Proof.
-intros n m p. rewrite (Zadd_comm p n); apply Zadd_add_simpl_l_l.
+intros n m p. rewrite (add_comm p n); apply add_add_simpl_l_l.
 Qed.
 
-Theorem Zadd_add_simpl_r_l : forall n m p : Z, (n + m) - (m + p) == n - p.
+Theorem add_add_simpl_r_l : forall n m p, (n + m) - (m + p) == n - p.
 Proof.
-intros n m p. rewrite (Zadd_comm n m); apply Zadd_add_simpl_l_l.
+intros n m p. rewrite (add_comm n m); apply add_add_simpl_l_l.
 Qed.
 
-Theorem Zadd_add_simpl_r_r : forall n m p : Z, (n + m) - (p + m) == n - p.
+Theorem add_add_simpl_r_r : forall n m p, (n + m) - (p + m) == n - p.
 Proof.
-intros n m p. rewrite (Zadd_comm p m); apply Zadd_add_simpl_r_l.
+intros n m p. rewrite (add_comm p m); apply add_add_simpl_r_l.
 Qed.
 
-Theorem Zsub_add_simpl_r_l : forall n m p : Z, (n - m) + (m + p) == n + p.
+Theorem sub_add_simpl_r_l : forall n m p, (n - m) + (m + p) == n + p.
 Proof.
-intros n m p. now rewrite <- Zsub_sub_distr, Zsub_add_distr, Zsub_diag,
-Zsub_0_l, Zsub_opp_r.
+intros n m p. now rewrite <- sub_sub_distr, sub_add_distr, sub_diag,
+sub_0_l, sub_opp_r.
 Qed.
 
-Theorem Zsub_add_simpl_r_r : forall n m p : Z, (n - m) + (p + m) == n + p.
+Theorem sub_add_simpl_r_r : forall n m p, (n - m) + (p + m) == n + p.
 Proof.
-intros n m p. rewrite (Zadd_comm p m); apply Zsub_add_simpl_r_l.
+intros n m p. rewrite (add_comm p m); apply sub_add_simpl_r_l.
 Qed.
 
-(* Of course, there are many other variants *)
+(** Of course, there are many other variants *)
 
 End ZAddPropFunct.
 
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 5f68b2bb15..282709c475 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -12,359 +12,289 @@
 
 Require Export ZLt.
 
-Module ZAddOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
-Open Local Scope IntScope.
+Module ZAddOrderPropFunct (Import Z : ZAxiomsSig).
+Include ZOrderPropFunct Z.
+Local Open Scope NumScope.
 
-(* Theorems that are true on both natural numbers and integers *)
+(** Theorems that are either not valid on N or have different proofs
+    on N and Z *)
 
-Theorem Zadd_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m.
-Proof NZadd_lt_mono_l.
-
-Theorem Zadd_lt_mono_r : forall n m p : Z, n < m <-> n + p < m + p.
-Proof NZadd_lt_mono_r.
-
-Theorem Zadd_lt_mono : forall n m p q : Z, n < m -> p < q -> n + p < m + q.
-Proof NZadd_lt_mono.
-
-Theorem Zadd_le_mono_l : forall n m p : Z, n <= m <-> p + n <= p + m.
-Proof NZadd_le_mono_l.
-
-Theorem Zadd_le_mono_r : forall n m p : Z, n <= m <-> n + p <= m + p.
-Proof NZadd_le_mono_r.
-
-Theorem Zadd_le_mono : forall n m p q : Z, n <= m -> p <= q -> n + p <= m + q.
-Proof NZadd_le_mono.
-
-Theorem Zadd_lt_le_mono : forall n m p q : Z, n < m -> p <= q -> n + p < m + q.
-Proof NZadd_lt_le_mono.
-
-Theorem Zadd_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q.
-Proof NZadd_le_lt_mono.
-
-Theorem Zadd_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m.
-Proof NZadd_pos_pos.
-
-Theorem Zadd_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m.
-Proof NZadd_pos_nonneg.
-
-Theorem Zadd_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m.
-Proof NZadd_nonneg_pos.
-
-Theorem Zadd_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m.
-Proof NZadd_nonneg_nonneg.
-
-Theorem Zlt_add_pos_l : forall n m : Z, 0 < n -> m < n + m.
-Proof NZlt_add_pos_l.
-
-Theorem Zlt_add_pos_r : forall n m : Z, 0 < n -> m < m + n.
-Proof NZlt_add_pos_r.
-
-Theorem Zle_lt_add_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q.
-Proof NZle_lt_add_lt.
-
-Theorem Zlt_le_add_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q.
-Proof NZlt_le_add_lt.
-
-Theorem Zle_le_add_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_le_add_le.
-
-Theorem Zadd_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q.
-Proof NZadd_lt_cases.
-
-Theorem Zadd_le_cases : forall n m p q : Z, n + m <= p + q -> n <= p \/ m <= q.
-Proof NZadd_le_cases.
-
-Theorem Zadd_neg_cases : forall n m : Z, n + m < 0 -> n < 0 \/ m < 0.
-Proof NZadd_neg_cases.
-
-Theorem Zadd_pos_cases : forall n m : Z, 0 < n + m -> 0 < n \/ 0 < m.
-Proof NZadd_pos_cases.
-
-Theorem Zadd_nonpos_cases : forall n m : Z, n + m <= 0 -> n <= 0 \/ m <= 0.
-Proof NZadd_nonpos_cases.
-
-Theorem Zadd_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
-Proof NZadd_nonneg_cases.
-
-(* Theorems that are either not valid on N or have different proofs on N and Z *)
-
-Theorem Zadd_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0.
+Theorem add_neg_neg : forall n m, n < 0 -> m < 0 -> n + m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_lt_mono.
 Qed.
 
-Theorem Zadd_neg_nonpos : forall n m : Z, n < 0 -> m <= 0 -> n + m < 0.
+Theorem add_neg_nonpos : forall n m, n < 0 -> m <= 0 -> n + m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_lt_le_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_lt_le_mono.
 Qed.
 
-Theorem Zadd_nonpos_neg : forall n m : Z, n <= 0 -> m < 0 -> n + m < 0.
+Theorem add_nonpos_neg : forall n m, n <= 0 -> m < 0 -> n + m < 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_lt_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_le_lt_mono.
 Qed.
 
-Theorem Zadd_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> n + m <= 0.
+Theorem add_nonpos_nonpos : forall n m, n <= 0 -> m <= 0 -> n + m <= 0.
 Proof.
-intros n m H1 H2. rewrite <- (Zadd_0_l 0). now apply Zadd_le_mono.
+intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_le_mono.
 Qed.
 
 (** Sub and order *)
 
-Theorem Zlt_0_sub : forall n m : Z, 0 < m - n <-> n < m.
+Theorem lt_0_sub : forall n m, 0 < m - n <-> n < m.
 Proof.
-intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zadd_lt_mono_r.
-rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
+intros n m. stepl (0 + n < m - n + n) by symmetry; apply add_lt_mono_r.
+rewrite add_0_l; now rewrite sub_simpl_r.
 Qed.
 
-Notation Zsub_pos := Zlt_0_sub (only parsing).
+Notation sub_pos := lt_0_sub (only parsing).
 
-Theorem Zle_0_sub : forall n m : Z, 0 <= m - n <-> n <= m.
+Theorem le_0_sub : forall n m, 0 <= m - n <-> n <= m.
 Proof.
-intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zadd_le_mono_r.
-rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
+intros n m; stepl (0 + n <= m - n + n) by symmetry; apply add_le_mono_r.
+rewrite add_0_l; now rewrite sub_simpl_r.
 Qed.
 
-Notation Zsub_nonneg := Zle_0_sub (only parsing).
+Notation sub_nonneg := le_0_sub (only parsing).
 
-Theorem Zlt_sub_0 : forall n m : Z, n - m < 0 <-> n < m.
+Theorem lt_sub_0 : forall n m, n - m < 0 <-> n < m.
 Proof.
-intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zadd_lt_mono_r.
-rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
+intros n m. stepl (n - m + m < 0 + m) by symmetry; apply add_lt_mono_r.
+rewrite add_0_l; now rewrite sub_simpl_r.
 Qed.
 
-Notation Zsub_neg := Zlt_sub_0 (only parsing).
+Notation sub_neg := lt_sub_0 (only parsing).
 
-Theorem Zle_sub_0 : forall n m : Z, n - m <= 0 <-> n <= m.
+Theorem le_sub_0 : forall n m, n - m <= 0 <-> n <= m.
 Proof.
-intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zadd_le_mono_r.
-rewrite Zadd_0_l; now rewrite Zsub_simpl_r.
+intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply add_le_mono_r.
+rewrite add_0_l; now rewrite sub_simpl_r.
 Qed.
 
-Notation Zsub_nonpos := Zle_sub_0 (only parsing).
+Notation sub_nonpos := le_sub_0 (only parsing).
 
-Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n.
+Theorem opp_lt_mono : forall n m, n < m <-> - m < - n.
 Proof.
-intros n m. stepr (m + - m < m + - n) by symmetry; apply Zadd_lt_mono_l.
-do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zlt_0_sub.
+intros n m. stepr (m + - m < m + - n) by symmetry; apply add_lt_mono_l.
+do 2 rewrite add_opp_r. rewrite sub_diag. symmetry; apply lt_0_sub.
 Qed.
 
-Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n.
+Theorem opp_le_mono : forall n m, n <= m <-> - m <= - n.
 Proof.
-intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zadd_le_mono_l.
-do 2 rewrite Zadd_opp_r. rewrite Zsub_diag. symmetry; apply Zle_0_sub.
+intros n m. stepr (m + - m <= m + - n) by symmetry; apply add_le_mono_l.
+do 2 rewrite add_opp_r. rewrite sub_diag. symmetry; apply le_0_sub.
 Qed.
 
-Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.
+Theorem opp_pos_neg : forall n, 0 < - n <-> n < 0.
 Proof.
-intro n; rewrite (Zopp_lt_mono n 0); now rewrite Zopp_0.
+intro n; rewrite (opp_lt_mono n 0); now rewrite opp_0.
 Qed.
 
-Theorem Zopp_neg_pos : forall n : Z, - n < 0 <-> 0 < n.
+Theorem opp_neg_pos : forall n, - n < 0 <-> 0 < n.
 Proof.
-intro n. rewrite (Zopp_lt_mono 0 n). now rewrite Zopp_0.
+intro n. rewrite (opp_lt_mono 0 n). now rewrite opp_0.
 Qed.
 
-Theorem Zopp_nonneg_nonpos : forall n : Z, 0 <= - n <-> n <= 0.
+Theorem opp_nonneg_nonpos : forall n, 0 <= - n <-> n <= 0.
 Proof.
-intro n; rewrite (Zopp_le_mono n 0); now rewrite Zopp_0.
+intro n; rewrite (opp_le_mono n 0); now rewrite opp_0.
 Qed.
 
-Theorem Zopp_nonpos_nonneg : forall n : Z, - n <= 0 <-> 0 <= n.
+Theorem opp_nonpos_nonneg : forall n, - n <= 0 <-> 0 <= n.
 Proof.
-intro n. rewrite (Zopp_le_mono 0 n). now rewrite Zopp_0.
+intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0.
 Qed.
 
-Theorem Zsub_lt_mono_l : forall n m p : Z, n < m <-> p - m < p - n.
+Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n.
 Proof.
-intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite <- Zadd_lt_mono_l.
-apply Zopp_lt_mono.
+intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l.
+apply opp_lt_mono.
 Qed.
 
-Theorem Zsub_lt_mono_r : forall n m p : Z, n < m <-> n - p < m - p.
+Theorem sub_lt_mono_r : forall n m p, n < m <-> n - p < m - p.
 Proof.
-intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_lt_mono_r.
+intros n m p; do 2 rewrite <- add_opp_r; apply add_lt_mono_r.
 Qed.
 
-Theorem Zsub_lt_mono : forall n m p q : Z, n < m -> q < p -> n - p < m - q.
+Theorem sub_lt_mono : forall n m p q, n < m -> q < p -> n - p < m - q.
 Proof.
 intros n m p q H1 H2.
-apply NZlt_trans with (m - p);
-[now apply -> Zsub_lt_mono_r | now apply -> Zsub_lt_mono_l].
+apply lt_trans with (m - p);
+[now apply -> sub_lt_mono_r | now apply -> sub_lt_mono_l].
 Qed.
 
-Theorem Zsub_le_mono_l : forall n m p : Z, n <= m <-> p - m <= p - n.
+Theorem sub_le_mono_l : forall n m p, n <= m <-> p - m <= p - n.
 Proof.
-intros n m p; do 2 rewrite <- Zadd_opp_r; rewrite <- Zadd_le_mono_l;
-apply Zopp_le_mono.
+intros n m p; do 2 rewrite <- add_opp_r; rewrite <- add_le_mono_l;
+apply opp_le_mono.
 Qed.
 
-Theorem Zsub_le_mono_r : forall n m p : Z, n <= m <-> n - p <= m - p.
+Theorem sub_le_mono_r : forall n m p, n <= m <-> n - p <= m - p.
 Proof.
-intros n m p; do 2 rewrite <- Zadd_opp_r; apply Zadd_le_mono_r.
+intros n m p; do 2 rewrite <- add_opp_r; apply add_le_mono_r.
 Qed.
 
-Theorem Zsub_le_mono : forall n m p q : Z, n <= m -> q <= p -> n - p <= m - q.
+Theorem sub_le_mono : forall n m p q, n <= m -> q <= p -> n - p <= m - q.
 Proof.
 intros n m p q H1 H2.
-apply NZle_trans with (m - p);
-[now apply -> Zsub_le_mono_r | now apply -> Zsub_le_mono_l].
+apply le_trans with (m - p);
+[now apply -> sub_le_mono_r | now apply -> sub_le_mono_l].
 Qed.
 
-Theorem Zsub_lt_le_mono : forall n m p q : Z, n < m -> q <= p -> n - p < m - q.
+Theorem sub_lt_le_mono : forall n m p q, n < m -> q <= p -> n - p < m - q.
 Proof.
 intros n m p q H1 H2.
-apply NZlt_le_trans with (m - p);
-[now apply -> Zsub_lt_mono_r | now apply -> Zsub_le_mono_l].
+apply lt_le_trans with (m - p);
+[now apply -> sub_lt_mono_r | now apply -> sub_le_mono_l].
 Qed.
 
-Theorem Zsub_le_lt_mono : forall n m p q : Z, n <= m -> q < p -> n - p < m - q.
+Theorem sub_le_lt_mono : forall n m p q, n <= m -> q < p -> n - p < m - q.
 Proof.
 intros n m p q H1 H2.
-apply NZle_lt_trans with (m - p);
-[now apply -> Zsub_le_mono_r | now apply -> Zsub_lt_mono_l].
+apply le_lt_trans with (m - p);
+[now apply -> sub_le_mono_r | now apply -> sub_lt_mono_l].
 Qed.
 
-Theorem Zle_lt_sub_lt : forall n m p q : Z, n <= m -> p - n < q - m -> p < q.
+Theorem le_lt_sub_lt : forall n m p q, n <= m -> p - n < q - m -> p < q.
 Proof.
-intros n m p q H1 H2. apply (Zle_lt_add_lt (- m) (- n));
-[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r].
+intros n m p q H1 H2. apply (le_lt_add_lt (- m) (- n));
+[now apply -> opp_le_mono | now do 2 rewrite add_opp_r].
 Qed.
 
-Theorem Zlt_le_sub_lt : forall n m p q : Z, n < m -> p - n <= q - m -> p < q.
+Theorem lt_le_sub_lt : forall n m p q, n < m -> p - n <= q - m -> p < q.
 Proof.
-intros n m p q H1 H2. apply (Zlt_le_add_lt (- m) (- n));
-[now apply -> Zopp_lt_mono | now do 2 rewrite Zadd_opp_r].
+intros n m p q H1 H2. apply (lt_le_add_lt (- m) (- n));
+[now apply -> opp_lt_mono | now do 2 rewrite add_opp_r].
 Qed.
 
-Theorem Zle_le_sub_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q.
+Theorem le_le_sub_lt : forall n m p q, n <= m -> p - n <= q - m -> p <= q.
 Proof.
-intros n m p q H1 H2. apply (Zle_le_add_le (- m) (- n));
-[now apply -> Zopp_le_mono | now do 2 rewrite Zadd_opp_r].
+intros n m p q H1 H2. apply (le_le_add_le (- m) (- n));
+[now apply -> opp_le_mono | now do 2 rewrite add_opp_r].
 Qed.
 
-Theorem Zlt_add_lt_sub_r : forall n m p : Z, n + p < m <-> n < m - p.
+Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
 Proof.
-intros n m p. stepl (n + p - p < m - p) by symmetry; apply Zsub_lt_mono_r.
-now rewrite Zadd_simpl_r.
+intros n m p. stepl (n + p - p < m - p) by symmetry; apply sub_lt_mono_r.
+now rewrite add_simpl_r.
 Qed.
 
-Theorem Zle_add_le_sub_r : forall n m p : Z, n + p <= m <-> n <= m - p.
+Theorem le_add_le_sub_r : forall n m p, n + p <= m <-> n <= m - p.
 Proof.
-intros n m p. stepl (n + p - p <= m - p) by symmetry; apply Zsub_le_mono_r.
-now rewrite Zadd_simpl_r.
+intros n m p. stepl (n + p - p <= m - p) by symmetry; apply sub_le_mono_r.
+now rewrite add_simpl_r.
 Qed.
 
-Theorem Zlt_add_lt_sub_l : forall n m p : Z, n + p < m <-> p < m - n.
+Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zlt_add_lt_sub_r.
+intros n m p. rewrite add_comm; apply lt_add_lt_sub_r.
 Qed.
 
-Theorem Zle_add_le_sub_l : forall n m p : Z, n + p <= m <-> p <= m - n.
+Theorem le_add_le_sub_l : forall n m p, n + p <= m <-> p <= m - n.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zle_add_le_sub_r.
+intros n m p. rewrite add_comm; apply le_add_le_sub_r.
 Qed.
 
-Theorem Zlt_sub_lt_add_r : forall n m p : Z, n - p < m <-> n < m + p.
+Theorem lt_sub_lt_add_r : forall n m p, n - p < m <-> n < m + p.
 Proof.
-intros n m p. stepl (n - p + p < m + p) by symmetry; apply Zadd_lt_mono_r.
-now rewrite Zsub_simpl_r.
+intros n m p. stepl (n - p + p < m + p) by symmetry; apply add_lt_mono_r.
+now rewrite sub_simpl_r.
 Qed.
 
-Theorem Zle_sub_le_add_r : forall n m p : Z, n - p <= m <-> n <= m + p.
+Theorem le_sub_le_add_r : forall n m p, n - p <= m <-> n <= m + p.
 Proof.
-intros n m p. stepl (n - p + p <= m + p) by symmetry; apply Zadd_le_mono_r.
-now rewrite Zsub_simpl_r.
+intros n m p. stepl (n - p + p <= m + p) by symmetry; apply add_le_mono_r.
+now rewrite sub_simpl_r.
 Qed.
 
-Theorem Zlt_sub_lt_add_l : forall n m p : Z, n - m < p <-> n < m + p.
+Theorem lt_sub_lt_add_l : forall n m p, n - m < p <-> n < m + p.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zlt_sub_lt_add_r.
+intros n m p. rewrite add_comm; apply lt_sub_lt_add_r.
 Qed.
 
-Theorem Zle_sub_le_add_l : forall n m p : Z, n - m <= p <-> n <= m + p.
+Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p.
 Proof.
-intros n m p. rewrite Zadd_comm; apply Zle_sub_le_add_r.
+intros n m p. rewrite add_comm; apply le_sub_le_add_r.
 Qed.
 
-Theorem Zlt_sub_lt_add : forall n m p q : Z, n - m < p - q <-> n + q < m + p.
+Theorem lt_sub_lt_add : forall n m p q, n - m < p - q <-> n + q < m + p.
 Proof.
-intros n m p q. rewrite Zlt_sub_lt_add_l. rewrite Zadd_sub_assoc.
-now rewrite <- Zlt_add_lt_sub_r.
+intros n m p q. rewrite lt_sub_lt_add_l. rewrite add_sub_assoc.
+now rewrite <- lt_add_lt_sub_r.
 Qed.
 
-Theorem Zle_sub_le_add : forall n m p q : Z, n - m <= p - q <-> n + q <= m + p.
+Theorem le_sub_le_add : forall n m p q, n - m <= p - q <-> n + q <= m + p.
 Proof.
-intros n m p q. rewrite Zle_sub_le_add_l. rewrite Zadd_sub_assoc.
-now rewrite <- Zle_add_le_sub_r.
+intros n m p q. rewrite le_sub_le_add_l. rewrite add_sub_assoc.
+now rewrite <- le_add_le_sub_r.
 Qed.
 
-Theorem Zlt_sub_pos : forall n m : Z, 0 < m <-> n - m < n.
+Theorem lt_sub_pos : forall n m, 0 < m <-> n - m < n.
 Proof.
-intros n m. stepr (n - m < n - 0) by now rewrite Zsub_0_r. apply Zsub_lt_mono_l.
+intros n m. stepr (n - m < n - 0) by now rewrite sub_0_r. apply sub_lt_mono_l.
 Qed.
 
-Theorem Zle_sub_nonneg : forall n m : Z, 0 <= m <-> n - m <= n.
+Theorem le_sub_nonneg : forall n m, 0 <= m <-> n - m <= n.
 Proof.
-intros n m. stepr (n - m <= n - 0) by now rewrite Zsub_0_r. apply Zsub_le_mono_l.
+intros n m. stepr (n - m <= n - 0) by now rewrite sub_0_r. apply sub_le_mono_l.
 Qed.
 
-Theorem Zsub_lt_cases : forall n m p q : Z, n - m < p - q -> n < m \/ q < p.
+Theorem sub_lt_cases : forall n m p q, n - m < p - q -> n < m \/ q < p.
 Proof.
-intros n m p q H. rewrite Zlt_sub_lt_add in H. now apply Zadd_lt_cases.
+intros n m p q H. rewrite lt_sub_lt_add in H. now apply add_lt_cases.
 Qed.
 
-Theorem Zsub_le_cases : forall n m p q : Z, n - m <= p - q -> n <= m \/ q <= p.
+Theorem sub_le_cases : forall n m p q, n - m <= p - q -> n <= m \/ q <= p.
 Proof.
-intros n m p q H. rewrite Zle_sub_le_add in H. now apply Zadd_le_cases.
+intros n m p q H. rewrite le_sub_le_add in H. now apply add_le_cases.
 Qed.
 
-Theorem Zsub_neg_cases : forall n m : Z, n - m < 0 -> n < 0 \/ 0 < m.
+Theorem sub_neg_cases : forall n m, n - m < 0 -> n < 0 \/ 0 < m.
 Proof.
-intros n m H; rewrite <- Zadd_opp_r in H.
-setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply Zopp_neg_pos).
-now apply Zadd_neg_cases.
+intros n m H; rewrite <- add_opp_r in H.
+setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply opp_neg_pos).
+now apply add_neg_cases.
 Qed.
 
-Theorem Zsub_pos_cases : forall n m : Z, 0 < n - m -> 0 < n \/ m < 0.
+Theorem sub_pos_cases : forall n m, 0 < n - m -> 0 < n \/ m < 0.
 Proof.
-intros n m H; rewrite <- Zadd_opp_r in H.
-setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply Zopp_pos_neg).
-now apply Zadd_pos_cases.
+intros n m H; rewrite <- add_opp_r in H.
+setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply opp_pos_neg).
+now apply add_pos_cases.
 Qed.
 
-Theorem Zsub_nonpos_cases : forall n m : Z, n - m <= 0 -> n <= 0 \/ 0 <= m.
+Theorem sub_nonpos_cases : forall n m, n - m <= 0 -> n <= 0 \/ 0 <= m.
 Proof.
-intros n m H; rewrite <- Zadd_opp_r in H.
-setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply Zopp_nonpos_nonneg).
-now apply Zadd_nonpos_cases.
+intros n m H; rewrite <- add_opp_r in H.
+setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply opp_nonpos_nonneg).
+now apply add_nonpos_cases.
 Qed.
 
-Theorem Zsub_nonneg_cases : forall n m : Z, 0 <= n - m -> 0 <= n \/ m <= 0.
+Theorem sub_nonneg_cases : forall n m, 0 <= n - m -> 0 <= n \/ m <= 0.
 Proof.
-intros n m H; rewrite <- Zadd_opp_r in H.
-setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply Zopp_nonneg_nonpos).
-now apply Zadd_nonneg_cases.
+intros n m H; rewrite <- add_opp_r in H.
+setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply opp_nonneg_nonpos).
+now apply add_nonneg_cases.
 Qed.
 
 Section PosNeg.
 
-Variable P : Z -> Prop.
-Hypothesis P_wd : Proper (Zeq ==> iff) P.
+Variable P : Z.t -> Prop.
+Hypothesis P_wd : Proper (Z.eq ==> iff) P.
 
-Theorem Z0_pos_neg :
-  P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n.
+Theorem zero_pos_neg :
+  P 0 -> (forall n, 0 < n -> P n /\ P (- n)) -> forall n, P n.
 Proof.
-intros H1 H2 n. destruct (Zlt_trichotomy n 0) as [H3 | [H3 | H3]].
-apply <- Zopp_pos_neg in H3. apply H2 in H3. destruct H3 as [_ H3].
-now rewrite Zopp_involutive in H3.
+intros H1 H2 n. destruct (lt_trichotomy n 0) as [H3 | [H3 | H3]].
+apply <- opp_pos_neg in H3. apply H2 in H3. destruct H3 as [_ H3].
+now rewrite opp_involutive in H3.
 now rewrite H3.
 apply H2 in H3; now destruct H3.
 Qed.
 
 End PosNeg.
 
-Ltac Z0_pos_neg n := induction_maker n ltac:(apply Z0_pos_neg).
+Ltac zero_pos_neg n := induction_maker n ltac:(apply zero_pos_neg).
 
 End ZAddOrderPropFunct.
 
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index bd6db10d9d..4acb45401d 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -15,51 +15,21 @@ Require Export NZAxioms.
 Set Implicit Arguments.
 
 Module Type ZAxiomsSig.
-Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
+Include Type NZOrdAxiomsSig.
+Local Open Scope NumScope.
 
-Delimit Scope IntScope with Int.
-Notation Z := NZ.
-Notation Zeq := NZeq.
-Notation Z0 := NZ0.
-Notation Z1 := (NZsucc NZ0).
-Notation S := NZsucc.
-Notation P := NZpred.
-Notation Zadd := NZadd.
-Notation Zmul := NZmul.
-Notation Zsub := NZsub.
-Notation Zlt := NZlt.
-Notation Zle := NZle.
-Notation Zmin := NZmin.
-Notation Zmax := NZmax.
-Notation "x == y"  := (NZeq x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
-Notation "0" := NZ0 : IntScope.
-Notation "1" := (NZsucc NZ0) : IntScope.
-Notation "x + y" := (NZadd x y) : IntScope.
-Notation "x - y" := (NZsub x y) : IntScope.
-Notation "x * y" := (NZmul x y) : IntScope.
-Notation "x < y" := (NZlt x y) : IntScope.
-Notation "x <= y" := (NZle x y) : IntScope.
-Notation "x > y" := (NZlt y x) (only parsing) : IntScope.
-Notation "x >= y" := (NZle y x) (only parsing) : IntScope.
+Parameter Inline opp : t -> t.
+Instance opp_wd : Proper (eq==>eq) opp.
 
-Parameter Zopp : Z -> Z.
-
-(*Notation "- 1" := (Zopp 1) : IntScope.
-Check (-1).*)
-
-Instance Zopp_wd : Proper (Zeq==>Zeq) Zopp.
-
-Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
-Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope.
-
-Open Local Scope IntScope.
+Notation "- x" := (opp x) (at level 35, right associativity) : NumScope.
+Notation "- 1" := (- (1)) : NumScope.
 
 (* Integers are obtained by postulating that every number has a predecessor *)
-Axiom Zsucc_pred : forall n : Z, S (P n) == n.
 
-Axiom Zopp_0 : - 0 == 0.
-Axiom Zopp_succ : forall n : Z, - (S n) == P (- n).
+Axiom succ_pred : forall n, S (P n) == n.
+
+Axiom opp_0 : - 0 == 0.
+Axiom opp_succ : forall n, - (S n) == P (- n).
 
 End ZAxiomsSig.
 
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 00e34a5b55..3429a4fa3d 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -12,74 +12,22 @@
 
 Require Export Decidable.
 Require Export ZAxioms.
-Require Import NZMulOrder.
+Require Import NZProperties.
 
-Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig).
-
-(* Note: writing "Export" instead of "Import" on the previous line leads to
-some warnings about hiding repeated declarations and results in the loss of
-notations in Zadd and later *)
-
-Open Local Scope IntScope.
-
-Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod.
-
-Theorem Zsucc_wd : forall n1 n2 : Z, n1 == n2 -> S n1 == S n2.
-Proof NZsucc_wd.
-
-Theorem Zpred_wd : forall n1 n2 : Z, n1 == n2 -> P n1 == P n2.
-Proof NZpred_wd.
-
-Theorem Zpred_succ : forall n : Z, P (S n) == n.
-Proof NZpred_succ.
-
-Theorem Zeq_refl : forall n : Z, n == n.
-Proof (@Equivalence_Reflexive _ _ NZeq_equiv).
-
-Theorem Zeq_sym : forall n m : Z, n == m -> m == n.
-Proof (@Equivalence_Symmetric _ _ NZeq_equiv).
-
-Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p.
-Proof (@Equivalence_Transitive _ _ NZeq_equiv).
-
-Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n.
-Proof NZneq_sym.
-
-Theorem Zsucc_inj : forall n1 n2 : Z, S n1 == S n2 -> n1 == n2.
-Proof NZsucc_inj.
-
-Theorem Zsucc_inj_wd : forall n1 n2 : Z, S n1 == S n2 <-> n1 == n2.
-Proof NZsucc_inj_wd.
-
-Theorem Zsucc_inj_wd_neg : forall n m : Z, S n ~= S m <-> n ~= m.
-Proof NZsucc_inj_wd_neg.
-
-(* Decidability and stability of equality was proved only in NZOrder, but
-since it does not mention order, we'll put it here *)
-
-Theorem Zeq_dec : forall n m : Z, decidable (n == m).
-Proof NZeq_dec.
-
-Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
-Proof NZeq_dne.
-
-Theorem Zcentral_induction :
-forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-  forall z : Z, A z ->
-    (forall n : Z, A n <-> A (S n)) ->
-      forall n : Z, A n.
-Proof NZcentral_induction.
+Module ZBasePropFunct (Import Z : ZAxiomsSig).
+Include NZPropFunct Z.
+Local Open Scope NumScope.
 
 (* Theorems that are true for integers but not for natural numbers *)
 
-Theorem Zpred_inj : forall n m : Z, P n == P m -> n == m.
+Theorem pred_inj : forall n m, P n == P m -> n == m.
 Proof.
-intros n m H. apply NZsucc_wd in H. now do 2 rewrite Zsucc_pred in H.
+intros n m H. apply succ_wd in H. now do 2 rewrite succ_pred in H.
 Qed.
 
-Theorem Zpred_inj_wd : forall n1 n2 : Z, P n1 == P n2 <-> n1 == n2.
+Theorem pred_inj_wd : forall n1 n2, P n1 == P n2 <-> n1 == n2.
 Proof.
-intros n1 n2; split; [apply Zpred_inj | apply NZpred_wd].
+intros n1 n2; split; [apply pred_inj | apply pred_wd].
 Qed.
 
 End ZBasePropFunct.
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
deleted file mode 100644
index 500dd9f535..0000000000
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ /dev/null
@@ -1,59 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*                      Evgeny Makarov, INRIA, 2007                     *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Import Bool.
-Require Export NumPrelude.
-
-Module Type ZDomainSignature.
-
-Parameter Inline Z : Set.
-Parameter Inline Zeq : Z -> Z -> Prop.
-Parameter Inline Zeqb : Z -> Z -> bool.
-
-Axiom eqb_equiv_eq : forall x y : Z, Zeqb x y = true <-> Zeq x y.
-Instance eq_equiv : Equivalence Zeq.
-
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with Z.
-Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
-Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope.
-
-End ZDomainSignature.
-
-Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
-Open Local Scope IntScope.
-
-Instance Zeqb_wd : Proper (Zeq ==> Zeq ==> eq) Zeqb.
-Proof.
-intros x x' Exx' y y' Eyy'.
-apply eq_true_iff_eq.
-rewrite 2 eqb_equiv_eq, Exx', Eyy'; auto with *.
-Qed.
-
-Theorem neq_sym : forall n m, n # m -> m # n.
-Proof.
-intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
-Qed.
-
-Theorem ZE_stepl : forall x y z : Z, x == y -> x == z -> z == y.
-Proof.
-intros x y z H1 H2; now rewrite <- H1.
-Qed.
-
-Declare Left Step ZE_stepl.
-
-(* The right step lemma is just transitivity of Zeq *)
-Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).
-
-End ZDomainProperties.
-
-
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index efd1f0da39..e77f9c453c 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -12,420 +12,123 @@
 
 Require Export ZMul.
 
-Module ZOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZMulPropMod := ZMulPropFunct ZAxiomsMod.
-Open Local Scope IntScope.
+Module ZOrderPropFunct (Import Z : ZAxiomsSig).
+Include ZMulPropFunct Z.
+Local Open Scope NumScope.
 
-(* Axioms *)
+(** Instances of earlier theorems for m == 0 *)
 
-Theorem Zlt_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 < m1 <-> n2 < m2).
-Proof NZlt_wd.
-
-Theorem Zle_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
-Proof NZle_wd.
-
-Theorem Zmin_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmin n1 m1 == Zmin n2 m2.
-Proof NZmin_wd.
-
-Theorem Zmax_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> Zmax n1 m1 == Zmax n2 m2.
-Proof NZmax_wd.
-
-Theorem Zlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m.
-Proof NZlt_eq_cases.
-
-Theorem Zlt_irrefl : forall n : Z, ~ n < n.
-Proof NZlt_irrefl.
-
-Theorem Zlt_succ_r : forall n m : Z, n < S m <-> n <= m.
-Proof NZlt_succ_r.
-
-Theorem Zmin_l : forall n m : Z, n <= m -> Zmin n m == n.
-Proof NZmin_l.
-
-Theorem Zmin_r : forall n m : Z, m <= n -> Zmin n m == m.
-Proof NZmin_r.
-
-Theorem Zmax_l : forall n m : Z, m <= n -> Zmax n m == n.
-Proof NZmax_l.
-
-Theorem Zmax_r : forall n m : Z, n <= m -> Zmax n m == m.
-Proof NZmax_r.
-
-(* Renaming theorems from NZOrder.v *)
-
-Theorem Zlt_le_incl : forall n m : Z, n < m -> n <= m.
-Proof NZlt_le_incl.
-
-Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m.
-Proof NZlt_neq.
-
-Theorem Zle_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m.
-Proof NZle_neq.
-
-Theorem Zle_refl : forall n : Z, n <= n.
-Proof NZle_refl.
-
-Theorem Zlt_succ_diag_r : forall n : Z, n < S n.
-Proof NZlt_succ_diag_r.
-
-Theorem Zle_succ_diag_r : forall n : Z, n <= S n.
-Proof NZle_succ_diag_r.
-
-Theorem Zlt_0_1 : 0 < 1.
-Proof NZlt_0_1.
-
-Theorem Zle_0_1 : 0 <= 1.
-Proof NZle_0_1.
-
-Theorem Zlt_lt_succ_r : forall n m : Z, n < m -> n < S m.
-Proof NZlt_lt_succ_r.
-
-Theorem Zle_le_succ_r : forall n m : Z, n <= m -> n <= S m.
-Proof NZle_le_succ_r.
-
-Theorem Zle_succ_r : forall n m : Z, n <= S m <-> n <= m \/ n == S m.
-Proof NZle_succ_r.
-
-Theorem Zneq_succ_diag_l : forall n : Z, S n ~= n.
-Proof NZneq_succ_diag_l.
-
-Theorem Zneq_succ_diag_r : forall n : Z, n ~= S n.
-Proof NZneq_succ_diag_r.
-
-Theorem Znlt_succ_diag_l : forall n : Z, ~ S n < n.
-Proof NZnlt_succ_diag_l.
-
-Theorem Znle_succ_diag_l : forall n : Z, ~ S n <= n.
-Proof NZnle_succ_diag_l.
-
-Theorem Zle_succ_l : forall n m : Z, S n <= m <-> n < m.
-Proof NZle_succ_l.
-
-Theorem Zlt_succ_l : forall n m : Z, S n < m -> n < m.
-Proof NZlt_succ_l.
-
-Theorem Zsucc_lt_mono : forall n m : Z, n < m <-> S n < S m.
-Proof NZsucc_lt_mono.
-
-Theorem Zsucc_le_mono : forall n m : Z, n <= m <-> S n <= S m.
-Proof NZsucc_le_mono.
-
-Theorem Zlt_asymm : forall n m, n < m -> ~ m < n.
-Proof NZlt_asymm.
-
-Notation Zlt_ngt := Zlt_asymm (only parsing).
-
-Theorem Zlt_trans : forall n m p : Z, n < m -> m < p -> n < p.
-Proof NZlt_trans.
-
-Theorem Zle_trans : forall n m p : Z, n <= m -> m <= p -> n <= p.
-Proof NZle_trans.
-
-Theorem Zle_lt_trans : forall n m p : Z, n <= m -> m < p -> n < p.
-Proof NZle_lt_trans.
-
-Theorem Zlt_le_trans : forall n m p : Z, n < m -> m <= p -> n < p.
-Proof NZlt_le_trans.
-
-Theorem Zle_antisymm : forall n m : Z, n <= m -> m <= n -> n == m.
-Proof NZle_antisymm.
-
-Theorem Zlt_1_l : forall n m : Z, 0 < n -> n < m -> 1 < m.
-Proof NZlt_1_l.
-
-(** Trichotomy, decidability, and double negation elimination *)
-
-Theorem Zlt_trichotomy : forall n m : Z,  n < m \/ n == m \/ m < n.
-Proof NZlt_trichotomy.
-
-Notation Zlt_eq_gt_cases := Zlt_trichotomy (only parsing).
-
-Theorem Zlt_gt_cases : forall n m : Z, n ~= m <-> n < m \/ n > m.
-Proof NZlt_gt_cases.
-
-Theorem Zle_gt_cases : forall n m : Z, n <= m \/ n > m.
-Proof NZle_gt_cases.
-
-Theorem Zlt_ge_cases : forall n m : Z, n < m \/ n >= m.
-Proof NZlt_ge_cases.
-
-Theorem Zle_ge_cases : forall n m : Z, n <= m \/ n >= m.
-Proof NZle_ge_cases.
-
-(** Instances of the previous theorems for m == 0 *)
-
-Theorem Zneg_pos_cases : forall n : Z, n ~= 0 <-> n < 0 \/ n > 0.
+Theorem neg_pos_cases : forall n, n ~= 0 <-> n < 0 \/ n > 0.
 Proof.
-intro; apply Zlt_gt_cases.
+intro; apply lt_gt_cases.
 Qed.
 
-Theorem Znonpos_pos_cases : forall n : Z, n <= 0 \/ n > 0.
+Theorem nonpos_pos_cases : forall n, n <= 0 \/ n > 0.
 Proof.
-intro; apply Zle_gt_cases.
+intro; apply le_gt_cases.
 Qed.
 
-Theorem Zneg_nonneg_cases : forall n : Z, n < 0 \/ n >= 0.
+Theorem neg_nonneg_cases : forall n, n < 0 \/ n >= 0.
 Proof.
-intro; apply Zlt_ge_cases.
+intro; apply lt_ge_cases.
 Qed.
 
-Theorem Znonpos_nonneg_cases : forall n : Z, n <= 0 \/ n >= 0.
+Theorem nonpos_nonneg_cases : forall n, n <= 0 \/ n >= 0.
 Proof.
-intro; apply Zle_ge_cases.
+intro; apply le_ge_cases.
 Qed.
 
-Theorem Zle_ngt : forall n m : Z, n <= m <-> ~ n > m.
-Proof NZle_ngt.
-
-Theorem Znlt_ge : forall n m : Z, ~ n < m <-> n >= m.
-Proof NZnlt_ge.
-
-Theorem Zlt_dec : forall n m : Z, decidable (n < m).
-Proof NZlt_dec.
-
-Theorem Zlt_dne : forall n m, ~ ~ n < m <-> n < m.
-Proof NZlt_dne.
-
-Theorem Znle_gt : forall n m : Z, ~ n <= m <-> n > m.
-Proof NZnle_gt.
-
-Theorem Zlt_nge : forall n m : Z, n < m <-> ~ n >= m.
-Proof NZlt_nge.
-
-Theorem Zle_dec : forall n m : Z, decidable (n <= m).
-Proof NZle_dec.
-
-Theorem Zle_dne : forall n m : Z, ~ ~ n <= m <-> n <= m.
-Proof NZle_dne.
-
-Theorem Znlt_succ_r : forall n m : Z, ~ m < S n <-> n < m.
-Proof NZnlt_succ_r.
-
-Theorem Zlt_exists_pred :
-  forall z n : Z, z < n -> exists k : Z, n == S k /\ z <= k.
-Proof NZlt_exists_pred.
-
-Theorem Zlt_succ_iter_r :
-  forall (n : nat) (m : Z), m < NZsucc_iter (Datatypes.S n) m.
-Proof NZlt_succ_iter_r.
-
-Theorem Zneq_succ_iter_l :
-  forall (n : nat) (m : Z), NZsucc_iter (Datatypes.S n) m ~= m.
-Proof NZneq_succ_iter_l.
-
-(** Stronger variant of induction with assumptions n >= 0 (n < 0)
-in the induction step *)
-
-Theorem Zright_induction :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z, A z ->
-      (forall n : Z, z <= n -> A n -> A (S n)) ->
-        forall n : Z, z <= n -> A n.
-Proof NZright_induction.
-
-Theorem Zleft_induction :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z, A z ->
-      (forall n : Z, n < z -> A (S n) -> A n) ->
-        forall n : Z, n <= z -> A n.
-Proof NZleft_induction.
-
-Theorem Zright_induction' :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z,
-      (forall n : Z, n <= z -> A n) ->
-      (forall n : Z, z <= n -> A n -> A (S n)) ->
-        forall n : Z, A n.
-Proof NZright_induction'.
-
-Theorem Zleft_induction' :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z,
-    (forall n : Z, z <= n -> A n) ->
-    (forall n : Z, n < z -> A (S n) -> A n) ->
-      forall n : Z, A n.
-Proof NZleft_induction'.
-
-Theorem Zstrong_right_induction :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z,
-    (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
-       forall n : Z, z <= n -> A n.
-Proof NZstrong_right_induction.
-
-Theorem Zstrong_left_induction :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z,
-      (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
-        forall n : Z, n <= z -> A n.
-Proof NZstrong_left_induction.
-
-Theorem Zstrong_right_induction' :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z,
-      (forall n : Z, n <= z -> A n) ->
-      (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
-        forall n : Z, A n.
-Proof NZstrong_right_induction'.
-
-Theorem Zstrong_left_induction' :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z,
-    (forall n : Z, z <= n -> A n) ->
-    (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
-      forall n : Z, A n.
-Proof NZstrong_left_induction'.
-
-Theorem Zorder_induction :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z, A z ->
-    (forall n : Z, z <= n -> A n -> A (S n)) ->
-    (forall n : Z, n < z -> A (S n) -> A n) ->
-      forall n : Z, A n.
-Proof NZorder_induction.
-
-Theorem Zorder_induction' :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall z : Z, A z ->
-    (forall n : Z, z <= n -> A n -> A (S n)) ->
-    (forall n : Z, n <= z -> A n -> A (P n)) ->
-      forall n : Z, A n.
-Proof NZorder_induction'.
-
-Theorem Zorder_induction_0 :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    A 0 ->
-    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
-    (forall n : Z, n < 0 -> A (S n) -> A n) ->
-      forall n : Z, A n.
-Proof NZorder_induction_0.
-
-Theorem Zorder_induction'_0 :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    A 0 ->
-    (forall n : Z, 0 <= n -> A n -> A (S n)) ->
-    (forall n : Z, n <= 0 -> A n -> A (P n)) ->
-      forall n : Z, A n.
-Proof NZorder_induction'_0.
-
-Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
-
-(** Elimintation principle for < *)
-
-Theorem Zlt_ind :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall n : Z, A (S n) ->
-      (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
-Proof NZlt_ind.
-
-(** Elimintation principle for <= *)
-
-Theorem Zle_ind :
-  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
-    forall n : Z, A n ->
-      (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
-Proof NZle_ind.
-
-(** Well-founded relations *)
-
-Theorem Zlt_wf : forall z : Z, well_founded (fun n m : Z => z <= n /\ n < m).
-Proof NZlt_wf.
-
-Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z).
-Proof NZgt_wf.
+Ltac zinduct n := induction_maker n ltac:(apply order_induction_0).
 
-(* Theorems that are either not valid on N or have different proofs on N and Z *)
+(** Theorems that are either not valid on N or have different proofs
+    on N and Z *)
 
-Theorem Zlt_pred_l : forall n : Z, P n < n.
+Theorem lt_pred_l : forall n, P n < n.
 Proof.
-intro n; rewrite <- (Zsucc_pred n) at 2; apply Zlt_succ_diag_r.
+intro n; rewrite <- (succ_pred n) at 2; apply lt_succ_diag_r.
 Qed.
 
-Theorem Zle_pred_l : forall n : Z, P n <= n.
+Theorem le_pred_l : forall n, P n <= n.
 Proof.
-intro; apply Zlt_le_incl; apply Zlt_pred_l.
+intro; apply lt_le_incl; apply lt_pred_l.
 Qed.
 
-Theorem Zlt_le_pred : forall n m : Z, n < m <-> n <= P m.
+Theorem lt_le_pred : forall n m, n < m <-> n <= P m.
 Proof.
-intros n m; rewrite <- (Zsucc_pred m); rewrite Zpred_succ. apply Zlt_succ_r.
+intros n m; rewrite <- (succ_pred m); rewrite pred_succ. apply lt_succ_r.
 Qed.
 
-Theorem Znle_pred_r : forall n : Z, ~ n <= P n.
+Theorem nle_pred_r : forall n, ~ n <= P n.
 Proof.
-intro; rewrite <- Zlt_le_pred; apply Zlt_irrefl.
+intro; rewrite <- lt_le_pred; apply lt_irrefl.
 Qed.
 
-Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m.
+Theorem lt_pred_le : forall n m, P n < m <-> n <= m.
 Proof.
-intros n m; rewrite <- (Zsucc_pred n) at 2.
-symmetry; apply Zle_succ_l.
+intros n m; rewrite <- (succ_pred n) at 2.
+symmetry; apply le_succ_l.
 Qed.
 
-Theorem Zlt_lt_pred : forall n m : Z, n < m -> P n < m.
+Theorem lt_lt_pred : forall n m, n < m -> P n < m.
 Proof.
-intros; apply <- Zlt_pred_le; now apply Zlt_le_incl.
+intros; apply <- lt_pred_le; now apply lt_le_incl.
 Qed.
 
-Theorem Zle_le_pred : forall n m : Z, n <= m -> P n <= m.
+Theorem le_le_pred : forall n m, n <= m -> P n <= m.
 Proof.
-intros; apply Zlt_le_incl; now apply <- Zlt_pred_le.
+intros; apply lt_le_incl; now apply <- lt_pred_le.
 Qed.
 
-Theorem Zlt_pred_lt : forall n m : Z, n < P m -> n < m.
+Theorem lt_pred_lt : forall n m, n < P m -> n < m.
 Proof.
-intros n m H; apply Zlt_trans with (P m); [assumption | apply Zlt_pred_l].
+intros n m H; apply lt_trans with (P m); [assumption | apply lt_pred_l].
 Qed.
 
-Theorem Zle_pred_lt : forall n m : Z, n <= P m -> n <= m.
+Theorem le_pred_lt : forall n m, n <= P m -> n <= m.
 Proof.
-intros; apply Zlt_le_incl; now apply <- Zlt_le_pred.
+intros; apply lt_le_incl; now apply <- lt_le_pred.
 Qed.
 
-Theorem Zpred_lt_mono : forall n m : Z, n < m <-> P n < P m.
+Theorem pred_lt_mono : forall n m, n < m <-> P n < P m.
 Proof.
-intros; rewrite Zlt_le_pred; symmetry; apply Zlt_pred_le.
+intros; rewrite lt_le_pred; symmetry; apply lt_pred_le.
 Qed.
 
-Theorem Zpred_le_mono : forall n m : Z, n <= m <-> P n <= P m.
+Theorem pred_le_mono : forall n m, n <= m <-> P n <= P m.
 Proof.
-intros; rewrite <- Zlt_pred_le; now rewrite Zlt_le_pred.
+intros; rewrite <- lt_pred_le; now rewrite lt_le_pred.
 Qed.
 
-Theorem Zlt_succ_lt_pred : forall n m : Z, S n < m <-> n < P m.
+Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.
 Proof.
-intros n m; now rewrite (Zpred_lt_mono (S n) m), Zpred_succ.
+intros n m; now rewrite (pred_lt_mono (S n) m), pred_succ.
 Qed.
 
-Theorem Zle_succ_le_pred : forall n m : Z, S n <= m <-> n <= P m.
+Theorem le_succ_le_pred : forall n m, S n <= m <-> n <= P m.
 Proof.
-intros n m; now rewrite (Zpred_le_mono (S n) m), Zpred_succ.
+intros n m; now rewrite (pred_le_mono (S n) m), pred_succ.
 Qed.
 
-Theorem Zlt_pred_lt_succ : forall n m : Z, P n < m <-> n < S m.
+Theorem lt_pred_lt_succ : forall n m, P n < m <-> n < S m.
 Proof.
-intros; rewrite Zlt_pred_le; symmetry; apply Zlt_succ_r.
+intros; rewrite lt_pred_le; symmetry; apply lt_succ_r.
 Qed.
 
-Theorem Zle_pred_lt_succ : forall n m : Z, P n <= m <-> n <= S m.
+Theorem le_pred_lt_succ : forall n m, P n <= m <-> n <= S m.
 Proof.
-intros n m; now rewrite (Zpred_le_mono n (S m)), Zpred_succ.
+intros n m; now rewrite (pred_le_mono n (S m)), pred_succ.
 Qed.
 
-Theorem Zneq_pred_l : forall n : Z, P n ~= n.
+Theorem neq_pred_l : forall n, P n ~= n.
 Proof.
-intro; apply Zlt_neq; apply Zlt_pred_l.
+intro; apply lt_neq; apply lt_pred_l.
 Qed.
 
-Theorem Zlt_n1_r : forall n m : Z, n < m -> m < 0 -> n < -1.
+Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -1.
 Proof.
-intros n m H1 H2. apply -> Zlt_le_pred in H2.
-setoid_replace (P 0) with (-1) in H2. now apply NZlt_le_trans with m.
-apply <- Zeq_opp_r. now rewrite Zopp_pred, Zopp_0.
+intros n m H1 H2. apply -> lt_le_pred in H2.
+setoid_replace (P 0) with (-1) in H2. now apply lt_le_trans with m.
+apply <- eq_opp_r. now rewrite opp_pred, opp_0.
 Qed.
 
 End ZOrderPropFunct.
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 785c0f41bd..4be2ac887b 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -12,102 +12,60 @@
 
 Require Export ZAdd.
 
-Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZAddPropMod := ZAddPropFunct ZAxiomsMod.
-Open Local Scope IntScope.
-
-Theorem Zmul_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2.
-Proof NZmul_wd.
-
-Theorem Zmul_0_l : forall n : Z, 0 * n == 0.
-Proof NZmul_0_l.
-
-Theorem Zmul_succ_l : forall n m : Z, (S n) * m == n * m + m.
-Proof NZmul_succ_l.
-
-(* Theorems that are valid for both natural numbers and integers *)
-
-Theorem Zmul_0_r : forall n : Z, n * 0 == 0.
-Proof NZmul_0_r.
-
-Theorem Zmul_succ_r : forall n m : Z, n * (S m) == n * m + n.
-Proof NZmul_succ_r.
-
-Theorem Zmul_comm : forall n m : Z, n * m == m * n.
-Proof NZmul_comm.
-
-Theorem Zmul_add_distr_r : forall n m p : Z, (n + m) * p == n * p + m * p.
-Proof NZmul_add_distr_r.
-
-Theorem Zmul_add_distr_l : forall n m p : Z, n * (m + p) == n * m + n * p.
-Proof NZmul_add_distr_l.
-
-(* A note on naming: right (correspondingly, left) distributivity happens
-when the sum is multiplied by a number on the right (left), not when the
-sum itself is the right (left) factor in the product (see planetmath.org
-and mathworld.wolfram.com). In the old library BinInt, distributivity over
-subtraction was named correctly, but distributivity over addition was named
-incorrectly. The names in Isabelle/HOL library are also incorrect. *)
-
-Theorem Zmul_assoc : forall n m p : Z, n * (m * p) == (n * m) * p.
-Proof NZmul_assoc.
-
-Theorem Zmul_1_l : forall n : Z, 1 * n == n.
-Proof NZmul_1_l.
-
-Theorem Zmul_1_r : forall n : Z, n * 1 == n.
-Proof NZmul_1_r.
-
-(* The following two theorems are true in an ordered ring,
-but since they don't mention order, we'll put them here *)
-
-Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
-Proof NZeq_mul_0.
-
-Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZneq_mul_0.
-
-(* Theorems that are either not valid on N or have different proofs on N and Z *)
-
-Theorem Zmul_pred_r : forall n m : Z, n * (P m) == n * m - n.
+Module ZMulPropFunct (Import Z : ZAxiomsSig).
+Include ZAddPropFunct Z.
+Local Open Scope NumScope.
+
+(** A note on naming: right (correspondingly, left) distributivity
+    happens when the sum is multiplied by a number on the right
+    (left), not when the sum itself is the right (left) factor in the
+    product (see planetmath.org and mathworld.wolfram.com). In the old
+    library BinInt, distributivity over subtraction was named
+    correctly, but distributivity over addition was named
+    incorrectly. The names in Isabelle/HOL library are also
+    incorrect. *)
+
+(** Theorems that are either not valid on N or have different proofs
+    on N and Z *)
+
+Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
 Proof.
 intros n m.
-rewrite <- (Zsucc_pred m) at 2.
-now rewrite Zmul_succ_r, <- Zadd_sub_assoc, Zsub_diag, Zadd_0_r.
+rewrite <- (succ_pred m) at 2.
+now rewrite mul_succ_r, <- add_sub_assoc, sub_diag, add_0_r.
 Qed.
 
-Theorem Zmul_pred_l : forall n m : Z, (P n) * m == n * m - m.
+Theorem mul_pred_l : forall n m, (P n) * m == n * m - m.
 Proof.
-intros n m; rewrite (Zmul_comm (P n) m), (Zmul_comm n m). apply Zmul_pred_r.
+intros n m; rewrite (mul_comm (P n) m), (mul_comm n m). apply mul_pred_r.
 Qed.
 
-Theorem Zmul_opp_l : forall n m : Z, (- n) * m == - (n * m).
+Theorem mul_opp_l : forall n m, (- n) * m == - (n * m).
 Proof.
-intros n m. apply -> Zadd_move_0_r.
-now rewrite <- Zmul_add_distr_r, Zadd_opp_diag_l, Zmul_0_l.
+intros n m. apply -> add_move_0_r.
+now rewrite <- mul_add_distr_r, add_opp_diag_l, mul_0_l.
 Qed.
 
-Theorem Zmul_opp_r : forall n m : Z, n * (- m) == - (n * m).
+Theorem mul_opp_r : forall n m, n * (- m) == - (n * m).
 Proof.
-intros n m; rewrite (Zmul_comm n (- m)), (Zmul_comm n m); apply Zmul_opp_l.
+intros n m; rewrite (mul_comm n (- m)), (mul_comm n m); apply mul_opp_l.
 Qed.
 
-Theorem Zmul_opp_opp : forall n m : Z, (- n) * (- m) == n * m.
+Theorem mul_opp_opp : forall n m, (- n) * (- m) == n * m.
 Proof.
-intros n m; now rewrite Zmul_opp_l, Zmul_opp_r, Zopp_involutive.
+intros n m; now rewrite mul_opp_l, mul_opp_r, opp_involutive.
 Qed.
 
-Theorem Zmul_sub_distr_l : forall n m p : Z, n * (m - p) == n * m - n * p.
+Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p.
 Proof.
-intros n m p. do 2 rewrite <- Zadd_opp_r. rewrite Zmul_add_distr_l.
-now rewrite Zmul_opp_r.
+intros n m p. do 2 rewrite <- add_opp_r. rewrite mul_add_distr_l.
+now rewrite mul_opp_r.
 Qed.
 
-Theorem Zmul_sub_distr_r : forall n m p : Z, (n - m) * p == n * p - m * p.
+Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
 Proof.
-intros n m p; rewrite (Zmul_comm (n - m) p), (Zmul_comm n p), (Zmul_comm m p);
-now apply Zmul_sub_distr_l.
+intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p);
+now apply mul_sub_distr_l.
 Qed.
 
 End ZMulPropFunct.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 74c893594e..4f11dcc5c0 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -12,331 +12,226 @@
 
 Require Export ZAddOrder.
 
-Module ZMulOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZAddOrderPropMod := ZAddOrderPropFunct ZAxiomsMod.
-Open Local Scope IntScope.
+Module ZMulOrderPropFunct (Import Z : ZAxiomsSig).
+Include ZAddOrderPropFunct Z.
+Local Open Scope NumScope.
 
-Theorem Zmul_lt_pred :
-  forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
-Proof NZmul_lt_pred.
-
-Theorem Zmul_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m).
-Proof NZmul_lt_mono_pos_l.
-
-Theorem Zmul_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p).
-Proof NZmul_lt_mono_pos_r.
-
-Theorem Zmul_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n).
-Proof NZmul_lt_mono_neg_l.
-
-Theorem Zmul_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p).
-Proof NZmul_lt_mono_neg_r.
-
-Theorem Zmul_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m.
-Proof NZmul_le_mono_nonneg_l.
-
-Theorem Zmul_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n.
-Proof NZmul_le_mono_nonpos_l.
-
-Theorem Zmul_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p.
-Proof NZmul_le_mono_nonneg_r.
-
-Theorem Zmul_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p.
-Proof NZmul_le_mono_nonpos_r.
-
-Theorem Zmul_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m).
-Proof NZmul_cancel_l.
-
-Theorem Zmul_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
-Proof NZmul_cancel_r.
-
-Theorem Zmul_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1).
-Proof NZmul_id_l.
-
-Theorem Zmul_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1).
-Proof NZmul_id_r.
-
-Theorem Zmul_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
-Proof NZmul_le_mono_pos_l.
-
-Theorem Zmul_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p).
-Proof NZmul_le_mono_pos_r.
-
-Theorem Zmul_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n).
-Proof NZmul_le_mono_neg_l.
-
-Theorem Zmul_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p).
-Proof NZmul_le_mono_neg_r.
-
-Theorem Zmul_lt_mono_nonneg :
-  forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q.
-Proof NZmul_lt_mono_nonneg.
-
-Theorem Zmul_lt_mono_nonpos :
-  forall n m p q : Z, m <= 0 -> n < m -> q <= 0 -> p < q ->  m * q < n * p.
+Theorem mul_lt_mono_nonpos :
+  forall n m p q, m <= 0 -> n < m -> q <= 0 -> p < q ->  m * q < n * p.
 Proof.
 intros n m p q H1 H2 H3 H4.
-apply Zle_lt_trans with (m * p).
-apply Zmul_le_mono_nonpos_l; [assumption | now apply Zlt_le_incl].
-apply -> Zmul_lt_mono_neg_r; [assumption | now apply Zlt_le_trans with q].
+apply le_lt_trans with (m * p).
+apply mul_le_mono_nonpos_l; [assumption | now apply lt_le_incl].
+apply -> mul_lt_mono_neg_r; [assumption | now apply lt_le_trans with q].
 Qed.
 
-Theorem Zmul_le_mono_nonneg :
-  forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q.
-Proof NZmul_le_mono_nonneg.
-
-Theorem Zmul_le_mono_nonpos :
-  forall n m p q : Z, m <= 0 -> n <= m -> q <= 0 -> p <= q ->  m * q <= n * p.
+Theorem mul_le_mono_nonpos :
+  forall n m p q, m <= 0 -> n <= m -> q <= 0 -> p <= q ->  m * q <= n * p.
 Proof.
 intros n m p q H1 H2 H3 H4.
-apply Zle_trans with (m * p).
-now apply Zmul_le_mono_nonpos_l.
-apply Zmul_le_mono_nonpos_r; [now apply Zle_trans with q | assumption].
+apply le_trans with (m * p).
+now apply mul_le_mono_nonpos_l.
+apply mul_le_mono_nonpos_r; [now apply le_trans with q | assumption].
 Qed.
 
-Theorem Zmul_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m.
-Proof NZmul_pos_pos.
-
-Theorem Zmul_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m.
-Proof NZmul_neg_neg.
-
-Theorem Zmul_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0.
-Proof NZmul_pos_neg.
-
-Theorem Zmul_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0.
-Proof NZmul_neg_pos.
-
-Theorem Zmul_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m.
+Theorem mul_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n * m.
 Proof.
 intros n m H1 H2.
-rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonneg_r.
+rewrite <- (mul_0_l m). now apply mul_le_mono_nonneg_r.
 Qed.
 
-Theorem Zmul_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m.
+Theorem mul_nonpos_nonpos : forall n m, n <= 0 -> m <= 0 -> 0 <= n * m.
 Proof.
 intros n m H1 H2.
-rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r.
+rewrite <- (mul_0_l m). now apply mul_le_mono_nonpos_r.
 Qed.
 
-Theorem Zmul_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0.
+Theorem mul_nonneg_nonpos : forall n m, 0 <= n -> m <= 0 -> n * m <= 0.
 Proof.
 intros n m H1 H2.
-rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonpos_r.
+rewrite <- (mul_0_l m). now apply mul_le_mono_nonpos_r.
 Qed.
 
-Theorem Zmul_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0.
+Theorem mul_nonpos_nonneg : forall n m, n <= 0 -> 0 <= m -> n * m <= 0.
 Proof.
-intros; rewrite Zmul_comm; now apply Zmul_nonneg_nonpos.
+intros; rewrite mul_comm; now apply mul_nonneg_nonpos.
 Qed.
 
-Theorem Zlt_1_mul_pos : forall n m : Z, 1 < n -> 0 < m -> 1 < n * m.
-Proof NZlt_1_mul_pos.
-
-Theorem Zeq_mul_0 : forall n m : Z, n * m == 0 <-> n == 0 \/ m == 0.
-Proof NZeq_mul_0.
-
-Theorem Zneq_mul_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
-Proof NZneq_mul_0.
-
-Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0.
-Proof NZeq_square_0.
-
-Theorem Zeq_mul_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
-Proof NZeq_mul_0_l.
+Notation mul_pos := lt_0_mul (only parsing).
 
-Theorem Zeq_mul_0_r : forall n m : Z, n * m == 0 -> n ~= 0 -> m == 0.
-Proof NZeq_mul_0_r.
-
-Theorem Zlt_0_mul : forall n m : Z, 0 < n * m <-> 0 < n /\ 0 < m \/ m < 0 /\ n < 0.
-Proof NZlt_0_mul.
-
-Notation Zmul_pos := Zlt_0_mul (only parsing).
-
-Theorem Zlt_mul_0 :
-  forall n m : Z, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0.
+Theorem lt_mul_0 :
+  forall n m, n * m < 0 <-> n < 0 /\ m > 0 \/ n > 0 /\ m < 0.
 Proof.
 intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]].
-destruct (Zlt_trichotomy n 0) as [H1 | [H1 | H1]];
-[| rewrite H1 in H; rewrite Zmul_0_l in H; false_hyp H Zlt_irrefl |];
-(destruct (Zlt_trichotomy m 0) as [H2 | [H2 | H2]];
-[| rewrite H2 in H; rewrite Zmul_0_r in H; false_hyp H Zlt_irrefl |]);
+destruct (lt_trichotomy n 0) as [H1 | [H1 | H1]];
+[| rewrite H1 in H; rewrite mul_0_l in H; false_hyp H lt_irrefl |];
+(destruct (lt_trichotomy m 0) as [H2 | [H2 | H2]];
+[| rewrite H2 in H; rewrite mul_0_r in H; false_hyp H lt_irrefl |]);
 try (left; now split); try (right; now split).
-assert (H3 : n * m > 0) by now apply Zmul_neg_neg.
-exfalso; now apply (Zlt_asymm (n * m) 0).
-assert (H3 : n * m > 0) by now apply Zmul_pos_pos.
-exfalso; now apply (Zlt_asymm (n * m) 0).
-now apply Zmul_neg_pos. now apply Zmul_pos_neg.
+assert (H3 : n * m > 0) by now apply mul_neg_neg.
+exfalso; now apply (lt_asymm (n * m) 0).
+assert (H3 : n * m > 0) by now apply mul_pos_pos.
+exfalso; now apply (lt_asymm (n * m) 0).
+now apply mul_neg_pos. now apply mul_pos_neg.
 Qed.
 
-Notation Zmul_neg := Zlt_mul_0 (only parsing).
+Notation mul_neg := lt_mul_0 (only parsing).
 
-Theorem Zle_0_mul :
-  forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0.
+Theorem le_0_mul :
+  forall n m, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0.
 Proof.
-assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
-intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
-rewrite Zlt_0_mul, Zeq_mul_0.
-pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
+assert (R : forall n, 0 == n <-> n == 0) by (intros; split; apply eq_sym).
+intros n m. repeat rewrite lt_eq_cases. repeat rewrite R.
+rewrite lt_0_mul, eq_mul_0.
+pose proof (lt_trichotomy n 0); pose proof (lt_trichotomy m 0). tauto.
 Qed.
 
-Notation Zmul_nonneg := Zle_0_mul (only parsing).
+Notation mul_nonneg := le_0_mul (only parsing).
 
-Theorem Zle_mul_0 :
-  forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.
+Theorem le_mul_0 :
+  forall n m, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.
 Proof.
-assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
-intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
-rewrite Zlt_mul_0, Zeq_mul_0.
-pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
+assert (R : forall n, 0 == n <-> n == 0) by (intros; split; apply eq_sym).
+intros n m. repeat rewrite lt_eq_cases. repeat rewrite R.
+rewrite lt_mul_0, eq_mul_0.
+pose proof (lt_trichotomy n 0); pose proof (lt_trichotomy m 0). tauto.
 Qed.
 
-Notation Zmul_nonpos := Zle_mul_0 (only parsing).
+Notation mul_nonpos := le_mul_0 (only parsing).
 
-Theorem Zle_0_square : forall n : Z, 0 <= n * n.
+Theorem le_0_square : forall n, 0 <= n * n.
 Proof.
-intro n; destruct (Zneg_nonneg_cases n).
-apply Zlt_le_incl; now apply Zmul_neg_neg.
-now apply Zmul_nonneg_nonneg.
+intro n; destruct (neg_nonneg_cases n).
+apply lt_le_incl; now apply mul_neg_neg.
+now apply mul_nonneg_nonneg.
 Qed.
 
-Notation Zsquare_nonneg := Zle_0_square (only parsing).
+Notation square_nonneg := le_0_square (only parsing).
 
-Theorem Znlt_square_0 : forall n : Z, ~ n * n < 0.
+Theorem nlt_square_0 : forall n, ~ n * n < 0.
 Proof.
-intros n H. apply -> Zlt_nge in H. apply H. apply Zsquare_nonneg.
+intros n H. apply -> lt_nge in H. apply H. apply square_nonneg.
 Qed.
 
-Theorem Zsquare_lt_mono_nonneg : forall n m : Z, 0 <= n -> n < m -> n * n < m * m.
-Proof NZsquare_lt_mono_nonneg.
-
-Theorem Zsquare_lt_mono_nonpos : forall n m : Z, n <= 0 -> m < n -> n * n < m * m.
+Theorem square_lt_mono_nonpos : forall n m, n <= 0 -> m < n -> n * n < m * m.
 Proof.
-intros n m H1 H2. now apply Zmul_lt_mono_nonpos.
+intros n m H1 H2. now apply mul_lt_mono_nonpos.
 Qed.
 
-Theorem Zsquare_le_mono_nonneg : forall n m : Z, 0 <= n -> n <= m -> n * n <= m * m.
-Proof NZsquare_le_mono_nonneg.
-
-Theorem Zsquare_le_mono_nonpos : forall n m : Z, n <= 0 -> m <= n -> n * n <= m * m.
+Theorem square_le_mono_nonpos : forall n m, n <= 0 -> m <= n -> n * n <= m * m.
 Proof.
-intros n m H1 H2. now apply Zmul_le_mono_nonpos.
+intros n m H1 H2. now apply mul_le_mono_nonpos.
 Qed.
 
-Theorem Zsquare_lt_simpl_nonneg : forall n m : Z, 0 <= m -> n * n < m * m -> n < m.
-Proof NZsquare_lt_simpl_nonneg.
-
-Theorem Zsquare_le_simpl_nonneg : forall n m : Z, 0 <= m -> n * n <= m * m -> n <= m.
-Proof NZsquare_le_simpl_nonneg.
-
-Theorem Zsquare_lt_simpl_nonpos : forall n m : Z, m <= 0 -> n * n < m * m -> m < n.
+Theorem square_lt_simpl_nonpos : forall n m, m <= 0 -> n * n < m * m -> m < n.
 Proof.
-intros n m H1 H2. destruct (Zle_gt_cases n 0).
-destruct (NZlt_ge_cases m n).
-assumption. assert (F : m * m <= n * n) by now apply Zsquare_le_mono_nonpos.
-apply -> NZle_ngt in F. false_hyp H2 F.
-now apply Zle_lt_trans with 0.
+intros n m H1 H2. destruct (le_gt_cases n 0).
+destruct (lt_ge_cases m n).
+assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonpos.
+apply -> le_ngt in F. false_hyp H2 F.
+now apply le_lt_trans with 0.
 Qed.
 
-Theorem Zsquare_le_simpl_nonpos : forall n m : NZ, m <= 0 -> n * n <= m * m -> m <= n.
+Theorem square_le_simpl_nonpos : forall n m, m <= 0 -> n * n <= m * m -> m <= n.
 Proof.
-intros n m H1 H2. destruct (NZle_gt_cases n 0).
-destruct (NZle_gt_cases m n).
-assumption. assert (F : m * m < n * n) by now apply Zsquare_lt_mono_nonpos.
-apply -> NZlt_nge in F. false_hyp H2 F.
-apply Zlt_le_incl; now apply NZle_lt_trans with 0.
+intros n m H1 H2. destruct (le_gt_cases n 0).
+destruct (le_gt_cases m n).
+assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonpos.
+apply -> lt_nge in F. false_hyp H2 F.
+apply lt_le_incl; now apply le_lt_trans with 0.
 Qed.
 
-Theorem Zmul_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
-Proof NZmul_2_mono_l.
-
-Theorem Zlt_1_mul_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m.
+Theorem lt_1_mul_neg : forall n m, n < -1 -> m < 0 -> 1 < n * m.
 Proof.
-intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1.
-apply <- Zopp_pos_neg in H2. rewrite Zmul_opp_l, Zmul_1_l in H1.
-now apply Zlt_1_l with (- m).
+intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1.
+apply <- opp_pos_neg in H2. rewrite mul_opp_l, mul_1_l in H1.
+now apply lt_1_l with (- m).
 assumption.
 Qed.
 
-Theorem Zlt_mul_n1_neg : forall n m : Z, 1 < n -> m < 0 -> n * m < -1.
+Theorem lt_mul_n1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1.
 Proof.
-intros n m H1 H2. apply -> (NZmul_lt_mono_neg_r m) in H1.
-rewrite Zmul_1_l in H1. now apply Zlt_n1_r with m.
+intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1.
+rewrite mul_1_l in H1. now apply lt_n1_r with m.
 assumption.
 Qed.
 
-Theorem Zlt_mul_n1_pos : forall n m : Z, n < -1 -> 0 < m -> n * m < -1.
+Theorem lt_mul_n1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1.
 Proof.
-intros n m H1 H2. apply -> (NZmul_lt_mono_pos_r m) in H1.
-rewrite Zmul_opp_l, Zmul_1_l in H1.
-apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m).
+intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1.
+rewrite mul_opp_l, mul_1_l in H1.
+apply <- opp_neg_pos in H2. now apply lt_n1_r with (- m).
 assumption.
 Qed.
 
-Theorem Zlt_1_mul_l : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem lt_1_mul_l : forall n m, 1 < n ->
+ n * m < -1 \/ n * m == 0 \/ 1 < n * m.
 Proof.
-intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
-left. now apply Zlt_mul_n1_neg.
-right; left; now rewrite H1, Zmul_0_r.
-right; right; now apply Zlt_1_mul_pos.
+intros n m H; destruct (lt_trichotomy m 0) as [H1 | [H1 | H1]].
+left. now apply lt_mul_n1_neg.
+right; left; now rewrite H1, mul_0_r.
+right; right; now apply lt_1_mul_pos.
 Qed.
 
-Theorem Zlt_n1_mul_r : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem lt_n1_mul_r : forall n m, n < -1 ->
+ n * m < -1 \/ n * m == 0 \/ 1 < n * m.
 Proof.
-intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
-right; right. now apply Zlt_1_mul_neg.
-right; left; now rewrite H1, Zmul_0_r.
-left. now apply Zlt_mul_n1_pos.
+intros n m H; destruct (lt_trichotomy m 0) as [H1 | [H1 | H1]].
+right; right. now apply lt_1_mul_neg.
+right; left; now rewrite H1, mul_0_r.
+left. now apply lt_mul_n1_pos.
 Qed.
 
-Theorem Zeq_mul_1 : forall n m : Z, n * m == 1 -> n == 1 \/ n == -1.
+Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.
 Proof.
 assert (F : ~ 1 < -1).
 intro H.
-assert (H1 : -1 < 0). apply <- Zopp_neg_pos. apply Zlt_succ_diag_r.
-assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_diag_l.
-Z0_pos_neg n.
-intros m H; rewrite Zmul_0_l in H; false_hyp H Zneq_succ_diag_r.
-intros n H; split; apply <- Zle_succ_l in H; le_elim H.
-intros m H1; apply (Zlt_1_mul_l n m) in H.
+assert (H1 : -1 < 0). apply <- opp_neg_pos. apply lt_succ_diag_r.
+assert (H2 : 1 < 0) by now apply lt_trans with (-1).
+false_hyp H2 nlt_succ_diag_l.
+zero_pos_neg n.
+intros m H; rewrite mul_0_l in H; false_hyp H neq_succ_diag_r.
+intros n H; split; apply <- le_succ_l in H; le_elim H.
+intros m H1; apply (lt_1_mul_l n m) in H.
 rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl.
+false_hyp H F. false_hyp H neq_succ_diag_l. false_hyp H lt_irrefl.
 intros; now left.
-intros m H1; apply (Zlt_1_mul_l n m) in H. rewrite Zmul_opp_l in H1;
-apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H.
-false_hyp H Zneq_succ_diag_l. false_hyp H F.
-intros; right; symmetry; now apply Zopp_wd.
+intros m H1; apply (lt_1_mul_l n m) in H. rewrite mul_opp_l in H1;
+apply -> eq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
+false_hyp H lt_irrefl. apply -> eq_opp_l in H. rewrite opp_0 in H.
+false_hyp H neq_succ_diag_l. false_hyp H F.
+intros; right; symmetry; now apply opp_wd.
 Qed.
 
-Theorem Zlt_mul_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n).
+Theorem lt_mul_diag_l : forall n m, n < 0 -> (1 < m <-> n * m < n).
 Proof.
-intros n m H. stepr (n * m < n * 1) by now rewrite Zmul_1_r.
-now apply Zmul_lt_mono_neg_l.
+intros n m H. stepr (n * m < n * 1) by now rewrite mul_1_r.
+now apply mul_lt_mono_neg_l.
 Qed.
 
-Theorem Zlt_mul_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m).
+Theorem lt_mul_diag_r : forall n m, 0 < n -> (1 < m <-> n < n * m).
 Proof.
-intros n m H. stepr (n * 1 < n * m) by now rewrite Zmul_1_r.
-now apply Zmul_lt_mono_pos_l.
+intros n m H. stepr (n * 1 < n * m) by now rewrite mul_1_r.
+now apply mul_lt_mono_pos_l.
 Qed.
 
-Theorem Zle_mul_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n).
+Theorem le_mul_diag_l : forall n m, n < 0 -> (1 <= m <-> n * m <= n).
 Proof.
-intros n m H. stepr (n * m <= n * 1) by now rewrite Zmul_1_r.
-now apply Zmul_le_mono_neg_l.
+intros n m H. stepr (n * m <= n * 1) by now rewrite mul_1_r.
+now apply mul_le_mono_neg_l.
 Qed.
 
-Theorem Zle_mul_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m).
+Theorem le_mul_diag_r : forall n m, 0 < n -> (1 <= m <-> n <= n * m).
 Proof.
-intros n m H. stepr (n * 1 <= n * m) by now rewrite Zmul_1_r.
-now apply Zmul_le_mono_pos_l.
+intros n m H. stepr (n * 1 <= n * m) by now rewrite mul_1_r.
+now apply mul_le_mono_pos_l.
 Qed.
 
-Theorem Zlt_mul_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p.
+Theorem lt_mul_r : forall n m p, 0 < n -> 1 < p -> n < m -> n < m * p.
 Proof.
-intros. stepl (n * 1) by now rewrite Zmul_1_r.
-apply Zmul_lt_mono_nonneg.
-now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption.
+intros. stepl (n * 1) by now rewrite mul_1_r.
+apply mul_lt_mono_nonneg.
+now apply lt_le_incl. assumption. apply le_0_1. assumption.
 Qed.
 
 End ZMulOrderPropFunct.
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
new file mode 100644
index 0000000000..eee5b0273a
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export ZAxioms ZMulOrder.
+
+(** This functor summarizes all known facts about Z.
+    For the moment it is only an alias to [ZMulOrderPropFunct], which
+    subsumes all others.
+*)
+
+Module ZPropFunct := ZMulOrderPropFunct.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index f7c423ebbc..6e8ca37ca9 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -11,7 +11,7 @@
 (*i $Id$ i*)
 
 Require Export BigN.
-Require Import ZMulOrder.
+Require Import ZProperties.
 Require Import ZSig.
 Require Import ZSigZAxioms.
 Require Import ZMake.
@@ -21,7 +21,7 @@ Module BigZ <: ZType := ZMake.Make BigN.
 (** Module [BigZ] implements [ZAxiomsSig] *)
 
 Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
-Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod.
+Module Export BigZPropMod := ZPropFunct BigZAxiomsMod.
 
 (** Notations about [BigZ] *)
 
@@ -32,7 +32,7 @@ Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
 
-Notation Local "0" := BigZ.zero : bigZ_scope.
+Local Notation "0" := BigZ.zero : bigZ_scope.
 Infix "+" := BigZ.add : bigZ_scope.
 Infix "-" := BigZ.sub : bigZ_scope.
 Notation "- x" := (BigZ.opp x) : bigZ_scope.
@@ -93,13 +93,13 @@ Lemma BigZring :
  ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
 Proof.
 constructor.
-exact Zadd_0_l.
-exact Zadd_comm.
-exact Zadd_assoc.
-exact Zmul_1_l.
-exact Zmul_comm.
-exact Zmul_assoc.
-exact Zmul_add_distr_r.
+exact add_0_l.
+exact add_comm.
+exact add_assoc.
+exact mul_1_l.
+exact mul_comm.
+exact mul_assoc.
+exact mul_add_distr_r.
 exact sub_opp.
 exact add_opp.
 Qed.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 9b55c771c9..0d8f8bf5d4 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,163 +10,86 @@
 
 (*i $Id$ i*)
 
-Require Import ZMulOrder.
+
+Require Import ZAxioms ZProperties.
 Require Import ZArith.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
+
+(** * Implementation of [ZAxiomsSig] by [BinInt.Z] *)
 
 Module ZBinAxiomsMod <: ZAxiomsSig.
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
-
-Definition NZ := Z.
-Definition NZeq := (@eq Z).
-Definition NZ0 := 0.
-Definition NZsucc := Zsucc'.
-Definition NZpred := Zpred'.
-Definition NZadd := Zplus.
-Definition NZsub := Zminus.
-Definition NZmul := Zmult.
-
-Instance NZeq_equiv : Equivalence NZeq.
-Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc.
-Program Instance NZpred_wd : Proper (eq==>eq) NZpred.
-Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd.
-Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub.
-Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul.
-
-Theorem NZpred_succ : forall n : Z, NZpred (NZsucc n) = n.
-Proof.
-exact Zpred'_succ'.
-Qed.
 
-Theorem NZinduction :
-  forall A : Z -> Prop, Proper (NZeq ==> iff) A ->
-    A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n.
+(** Bi-directional induction. *)
+
+Theorem bi_induction :
+  forall A : Z -> Prop, Proper (eq ==> iff) A ->
+    A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
 Proof.
 intros A A_wd A0 AS n; apply Zind; clear n.
 assumption.
-intros; now apply -> AS.
-intros n H. rewrite <- (Zsucc'_pred' n) in H. now apply <- AS.
-Qed.
-
-Theorem NZadd_0_l : forall n : Z, 0 + n = n.
-Proof.
-exact Zplus_0_l.
-Qed.
-
-Theorem NZadd_succ_l : forall n m : Z, (NZsucc n) + m = NZsucc (n + m).
-Proof.
-intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l.
-Qed.
-
-Theorem NZsub_0_r : forall n : Z, n - 0 = n.
-Proof.
-exact Zminus_0_r.
-Qed.
-
-Theorem NZsub_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m).
-Proof.
-intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred';
-apply Zminus_succ_r.
-Qed.
-
-Theorem NZmul_0_l : forall n : Z, 0 * n = 0.
-Proof.
-reflexivity.
-Qed.
-
-Theorem NZmul_succ_l : forall n m : Z, (NZsucc n) * m = n * m + m.
-Proof.
-intros; rewrite <- Zsucc_succ'; apply Zmult_succ_l.
-Qed.
-
-End NZAxiomsMod.
-
-Definition NZlt := Zlt.
-Definition NZle := Zle.
-Definition NZmin := Zmin.
-Definition NZmax := Zmax.
-
-Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt.
-Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle.
-Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin.
-Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax.
-
-Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n = m.
-Proof.
-intros n m; split. apply Zle_lt_or_eq.
-intro H; destruct H as [H | H]. now apply Zlt_le_weak. rewrite H; apply Zle_refl.
+intros; rewrite <- Zsucc_succ'. now apply -> AS.
+intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS.
 Qed.
 
-Theorem NZlt_irrefl : forall n : Z, ~ n < n.
-Proof.
-exact Zlt_irrefl.
-Qed.
+(** Basic operations. *)
 
-Theorem NZlt_succ_r : forall n m : Z, n < (NZsucc m) <-> n <= m.
-Proof.
-intros; unfold NZsucc; rewrite <- Zsucc_succ'; split;
-[apply Zlt_succ_le | apply Zle_lt_succ].
-Qed.
+Instance eq_equiv : Equivalence (@eq Z).
+Program Instance succ_wd : Proper (eq==>eq) Zsucc.
+Program Instance pred_wd : Proper (eq==>eq) Zpred.
+Program Instance add_wd : Proper (eq==>eq==>eq) Zplus.
+Program Instance sub_wd : Proper (eq==>eq==>eq) Zminus.
+Program Instance mul_wd : Proper (eq==>eq==>eq) Zmult.
 
-Theorem NZmin_l : forall n m : NZ, n <= m -> NZmin n m = n.
-Proof.
-unfold NZmin, Zmin, Zle; intros n m H.
-destruct (n ?= m); try reflexivity. now elim H.
-Qed.
+Definition pred_succ n := eq_sym (Zpred_succ n).
+Definition add_0_l := Zplus_0_l.
+Definition add_succ_l := Zplus_succ_l.
+Definition sub_0_r := Zminus_0_r.
+Definition sub_succ_r := Zminus_succ_r.
+Definition mul_0_l := Zmult_0_l.
+Definition mul_succ_l := Zmult_succ_l.
 
-Theorem NZmin_r : forall n m : NZ, m <= n -> NZmin n m = m.
-Proof.
-unfold NZmin, Zmin, Zle; intros n m H.
-case_eq (n ?= m); intro H1; try reflexivity.
-now apply Zcompare_Eq_eq.
-apply <- Zcompare_Gt_Lt_antisym in H1. now elim H.
-Qed.
+(** Order *)
 
-Theorem NZmax_l : forall n m : NZ, m <= n -> NZmax n m = n.
-Proof.
-unfold NZmax, Zmax, Zle; intros n m H.
-case_eq (n ?= m); intro H1; try reflexivity.
-apply <- Zcompare_Gt_Lt_antisym in H1. now elim H.
-Qed.
+Program Instance lt_wd : Proper (eq==>eq==>iff) Zlt.
 
-Theorem NZmax_r : forall n m : NZ, n <= m -> NZmax n m = m.
-Proof.
-unfold NZmax, Zmax, Zle; intros n m H.
-case_eq (n ?= m); intro H1.
-now apply Zcompare_Eq_eq. reflexivity. now elim H.
-Qed.
+Definition lt_eq_cases := Zle_lt_or_eq_iff.
+Definition lt_irrefl := Zlt_irrefl.
+Definition lt_succ_r := Zlt_succ_r.
 
-End NZOrdAxiomsMod.
+Definition min_l := Zmin_l.
+Definition min_r := Zmin_r.
+Definition max_l := Zmax_l.
+Definition max_r := Zmax_r.
 
-Definition Zopp (x : Z) :=
-match x with
-| Z0 => Z0
-| Zpos x => Zneg x
-| Zneg x => Zpos x
-end.
+(** Properties specific to integers, not natural numbers. *)
 
-Program Instance Zopp_wd : Proper (eq==>eq) Zopp.
+Program Instance opp_wd : Proper (eq==>eq) Zopp.
 
-Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n.
-Proof.
-exact Zsucc'_pred'.
-Qed.
+Definition succ_pred n := eq_sym (Zsucc_pred n).
+Definition opp_0 := Zopp_0.
+Definition opp_succ := Zopp_succ.
 
-Theorem Zopp_0 : - 0 = 0.
-Proof.
-reflexivity.
-Qed.
+(** The instantiation of operations.
+    Placing them at the very end avoids having indirections in above lemmas. *)
 
-Theorem Zopp_succ : forall n : Z, - (NZsucc n) = NZpred (- n).
-Proof.
-intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'. apply Zopp_succ.
-Qed.
+Definition t := Z.
+Definition eq := (@eq Z).
+Definition zero := 0.
+Definition succ := Zsucc.
+Definition pred := Zpred.
+Definition add := Zplus.
+Definition sub := Zminus.
+Definition mul := Zmult.
+Definition lt := Zlt.
+Definition le := Zle.
+Definition min := Zmin.
+Definition max := Zmax.
+Definition opp := Zopp.
 
 End ZBinAxiomsMod.
 
-Module Export ZBinMulOrderPropMod := ZMulOrderPropFunct ZBinAxiomsMod.
+Module Export ZBinPropMod := ZPropFunct ZBinAxiomsMod.
 
 (** Z forms a ring *)
 
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index dcda3f1e59..0956f337f3 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -10,195 +10,150 @@
 
 (*i $Id$ i*)
 
-Require Import NSub. (* The most complete file for natural numbers *)
-Require Export ZMulOrder. (* The most complete file for integers *)
+Require Import NProperties. (* The most complete file for N *)
+Require Export ZProperties. (* The most complete file for Z *)
 Require Export Ring.
 
-Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig.
-Module Import NPropMod := NSubPropFunct NAxiomsMod. (* Get all properties of natural numbers *)
-
-(* We do not declare ring in Natural/Abstract for two reasons. First, some
-of the properties proved in NAdd and NMul are used in the new BinNat,
-and it is in turn used in Ring. Using ring in Natural/Abstract would be
-circular. It is possible, however, not to make BinNat dependent on
-Numbers/Natural and prove the properties necessary for ring from scratch
-(this is, of course, how it used to be). In addition, if we define semiring
-structures in the implementation subdirectories of Natural, we are able to
-specify binary natural numbers as the type of coefficients. For these
-reasons we define an abstract semiring here. *)
-
-Open Local Scope NatScope.
-
-Lemma Nsemi_ring : semi_ring_theory 0 1 add mul Neq.
-Proof.
-constructor.
-exact add_0_l.
-exact add_comm.
-exact add_assoc.
-exact mul_1_l.
-exact mul_0_l.
-exact mul_comm.
-exact mul_assoc.
-exact mul_add_distr_r.
-Qed.
-
-Add Ring NSR : Nsemi_ring.
-
-(* The definitions of functions (NZadd, NZmul, etc.) will be unfolded by
-the properties functor. Since we don't want Zadd_comm to refer to unfolded
-definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
-we will provide an extra layer of definitions. *)
-
-Definition Z := (N * N)%type.
-Definition Z0 : Z := (0, 0).
-Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
-Definition Zsucc (n : Z) : Z := (S (fst n), snd n).
-Definition Zpred (n : Z) : Z := (fst n, S (snd n)).
-
-(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) == n. It
-could be possible to consider as canonical only pairs where one of the
-elements is 0, and make all operations convert canonical values into other
-canonical values. In that case, we could get rid of setoids and arrive at
-integers as signed natural numbers. *)
-
-Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)).
-Definition Zsub (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)).
-
-(* Unfortunately, the elements of the pair keep increasing, even during
-subtraction *)
-
-Definition Zmul (n m : Z) : Z :=
-  ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
-Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n).
-Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n).
-Definition Zmin (n m : Z) := (min ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).
-Definition Zmax (n m : Z) := (max ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)).
+Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
+Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
+Open Local Scope pair_scope.
+
+Module ZPairsAxiomsMod (Import N : NAxiomsSig) <: ZAxiomsSig.
+Module Import NPropMod := NPropFunct N. (* Get all properties of N *)
+
+Local Open Scope NumScope.
+
+(** The definitions of functions ([add], [mul], etc.) will be unfolded
+    by the properties functor. Since we don't want [add_comm] to refer
+    to unfolded definitions of equality: [fun p1 p2 => (fst p1 +
+    snd p2) = (fst p2 + snd p1)], we will provide an extra layer of
+    definitions. *)
+
+Module Z.
+
+Definition t := (N.t * N.t)%type.
+Definition zero : t := (0, 0).
+Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2).
+Definition succ (n : t) : t := (S n#1, n#2).
+Definition pred (n : t) : t := (n#1, S n#2).
+Definition opp (n : t) : t := (n#2, n#1).
+Definition add (n m : t) : t := (n#1 + m#1, n#2 + m#2).
+Definition sub (n m : t) : t := (n#1 + m#2, n#2 + m#1).
+Definition mul (n m : t) : t :=
+  (n#1 * m#1 + n#2 * m#2, n#1 * m#2 + n#2 * m#1).
+Definition lt (n m : t) := n#1 + m#2 < m#1 + n#2.
+Definition le (n m : t) := n#1 + m#2 <= m#1 + n#2.
+Definition min (n m : t) : t := (min (n#1 + m#2) (m#1 + n#2), n#2 + m#2).
+Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2).
+
+(** NB : We do not have [Zpred (Zsucc n) = n] but only [Zpred (Zsucc n) == n].
+    It could be possible to consider as canonical only pairs where
+    one of the elements is 0, and make all operations convert
+    canonical values into other canonical values. In that case, we
+    could get rid of setoids and arrive at integers as signed natural
+    numbers. *)
+
+(** NB : Unfortunately, the elements of the pair keep increasing during
+    many operations, even during subtraction. *)
+
+End Z.
 
 Delimit Scope IntScope with Int.
-Bind Scope IntScope with Z.
-Notation "x == y"  := (Zeq x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope.
-Notation "0" := Z0 : IntScope.
-Notation "1" := (Zsucc Z0) : IntScope.
-Notation "x + y" := (Zadd x y) : IntScope.
-Notation "x - y" := (Zsub x y) : IntScope.
-Notation "x * y" := (Zmul x y) : IntScope.
-Notation "x < y" := (Zlt x y) : IntScope.
-Notation "x <= y" := (Zle x y) : IntScope.
-Notation "x > y" := (Zlt y x) (only parsing) : IntScope.
-Notation "x >= y" := (Zle y x) (only parsing) : IntScope.
-
-Notation Local N := NZ.
-(* To remember N without having to use a long qualifying name. since NZ will be redefined *)
-Notation Local NE := NZeq (only parsing).
-Notation Local add_wd := NZadd_wd (only parsing).
-
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
-
-Definition NZ : Type := Z.
-Definition NZeq := Zeq.
-Definition NZ0 := Z0.
-Definition NZsucc := Zsucc.
-Definition NZpred := Zpred.
-Definition NZadd := Zadd.
-Definition NZsub := Zsub.
-Definition NZmul := Zmul.
-
-Theorem ZE_refl : reflexive Z Zeq.
-Proof.
-unfold reflexive, Zeq. reflexivity.
-Qed.
+Bind Scope IntScope with Z.t.
+Notation "x == y"  := (Z.eq x y) (at level 70) : IntScope.
+Notation "x ~= y" := (~ Z.eq x y) (at level 70) : IntScope.
+Notation "0" := Z.zero : IntScope.
+Notation "1" := (Z.succ Z.zero) : IntScope.
+Notation "x + y" := (Z.add x y) : IntScope.
+Notation "x - y" := (Z.sub x y) : IntScope.
+Notation "x * y" := (Z.mul x y) : IntScope.
+Notation "- x" := (Z.opp x) : IntScope.
+Notation "x < y" := (Z.lt x y) : IntScope.
+Notation "x <= y" := (Z.le x y) : IntScope.
+Notation "x > y" := (Z.lt y x) (only parsing) : IntScope.
+Notation "x >= y" := (Z.le y x) (only parsing) : IntScope.
+
+Lemma sub_add_opp : forall n m, Z.sub n m = Z.add n (Z.opp m).
+Proof. reflexivity. Qed.
 
-Theorem ZE_sym : symmetric Z Zeq.
+Instance eq_equiv : Equivalence Z.eq.
 Proof.
-unfold symmetric, Zeq; now symmetry.
+split.
+unfold Reflexive, Z.eq. reflexivity.
+unfold Symmetric, Z.eq; now symmetry.
+unfold Transitive, Z.eq. intros (n1,n2) (m1,m2) (p1,p2) H1 H2; simpl in *.
+apply (add_cancel_r _ _ (m1+m2)).
+rewrite add_shuffle2, H1, add_shuffle1, H2.
+now rewrite add_shuffle1, (add_comm m1).
 Qed.
 
-Theorem ZE_trans : transitive Z Zeq.
+Instance pair_wd : Proper (N.eq==>N.eq==>Z.eq) (@pair N.t N.t).
 Proof.
-unfold transitive, Zeq. intros n m p H1 H2.
-assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m))
-by now apply add_wd.
-stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring.
-stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
-now apply -> add_cancel_r in H3.
+intros n1 n2 H1 m1 m2 H2; unfold Z.eq; simpl; now rewrite H1, H2.
 Qed.
 
-Instance NZeq_equiv : Equivalence Zeq.
+Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ.
 Proof.
-split; [apply ZE_refl | apply ZE_sym | apply ZE_trans].
+unfold Z.succ, Z.eq; intros n m H; simpl.
+do 2 rewrite add_succ_l; now rewrite H.
 Qed.
 
-Instance Zpair_wd : Proper (NE==>NE==>Zeq) (@pair N N).
+Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred.
 Proof.
-intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
+unfold Z.pred, Z.eq; intros n m H; simpl.
+do 2 rewrite add_succ_r; now rewrite H.
 Qed.
 
-Instance NZsucc_wd : Proper (Zeq ==> Zeq) NZsucc.
+Instance add_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add.
 Proof.
-unfold NZsucc, Zeq; intros n m H; simpl.
-do 2 rewrite add_succ_l; now rewrite H.
+unfold Z.eq, Z.add; intros n1 m1 H1 n2 m2 H2; simpl.
+now rewrite add_shuffle1, H1, H2, add_shuffle1.
 Qed.
 
-Instance NZpred_wd : Proper (Zeq ==> Zeq) NZpred.
+Instance opp_wd : Proper (Z.eq ==> Z.eq) Z.opp.
 Proof.
-unfold NZpred, Zeq; intros n m H; simpl.
-do 2 rewrite add_succ_r; now rewrite H.
+unfold Z.eq, Z.opp; intros (n1,n2) (m1,m2) H; simpl in *.
+now rewrite (add_comm n2), (add_comm m2).
 Qed.
 
-Instance NZadd_wd : Proper (Zeq ==> Zeq ==> Zeq) NZadd.
+Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub.
 Proof.
-unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl.
-assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
-by now apply add_wd.
-stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
-now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
+intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp.
+apply add_wd, opp_wd; auto.
 Qed.
 
-Instance NZsub_wd : Proper (Zeq ==> Zeq ==> Zeq) NZsub.
+Lemma mul_comm : forall n m, (n*m == m*n)%Int.
 Proof.
-unfold Zeq, NZsub; intros n1 m1 H1 n2 m2 H2; simpl.
-symmetry in H2.
-assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2))
-by now apply add_wd.
-stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
-now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
+intros (n1,n2) (m1,m2); compute.
+rewrite (add_comm (m1*n2)).
+apply N.add_wd; apply N.add_wd; apply mul_comm.
 Qed.
 
-Instance NZmul_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmul.
+Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul.
 Proof.
-unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
-stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
-stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring.
-apply add_mul_repl_pair with (n := fst m2) (m := snd m2); [| now idtac].
-stepl (snd n1 * snd n2 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
-stepr (snd n1 * fst n2 + (fst n1 * snd m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply add_mul_repl_pair with (n := snd m2) (m := fst m2);
-[| (stepl (fst n2 + snd m2) by ring); now stepr (fst m2 + snd n2) by ring].
-stepl (snd m2 * snd n1 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
-stepr (snd m2 * fst n1 + (snd n1 * fst m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply add_mul_repl_pair with (n := snd m1) (m := fst m1);
-[ | (stepl (fst n1 + snd m1) by ring); now stepr (fst m1 + snd n1) by ring].
-stepl (fst m2 * fst n1 + (snd m2 * snd m1 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
-stepr (fst m2 * snd n1 + (snd m2 * fst m1 + fst m1 * fst m2 + snd m1 * snd m2)) by ring.
-apply add_mul_repl_pair with (n := fst m1) (m := snd m1); [| now idtac].
-ring.
+assert (forall n, Proper (Z.eq ==> Z.eq) (Z.mul n)).
+ unfold Z.mul, Z.eq. intros (n1,n2) (p1,p2) (q1,q2) H; simpl in *.
+ rewrite add_shuffle1, (add_comm (n1*p1)).
+ symmetry. rewrite add_shuffle1.
+ rewrite <- ! mul_add_distr_l.
+ rewrite (add_comm p2), (add_comm q2), H.
+ reflexivity.
+intros n n' Hn m m' Hm.
+rewrite Hm, (mul_comm n), (mul_comm n'), Hn.
+reflexivity.
 Qed.
 
 Section Induction.
-Open Scope NatScope. (* automatically closes at the end of the section *)
-Variable A : Z -> Prop.
-Hypothesis A_wd : Proper (Zeq==>iff) A.
+Variable A : Z.t -> Prop.
+Hypothesis A_wd : Proper (Z.eq==>iff) A.
 
-Theorem NZinduction :
-  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
-  (* 0 is interpreted as in Z due to "Bind" directive *)
+Theorem bi_induction :
+  A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n.
 Proof.
-intros A0 AS n; unfold NZ0, Zsucc, Zeq in *.
+intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *.
 destruct n as [n m].
-cut (forall p : N, A (p, 0)); [intro H1 |].
-cut (forall p : N, A (0, p)); [intro H2 |].
+cut (forall p, A (p, 0)); [intro H1 |].
+cut (forall p, A (0, p)); [intro H2 |].
 destruct (add_dichotomy n m) as [[p H] | [p H]].
 rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
 apply H2.
@@ -215,183 +170,136 @@ End Induction.
 
 (* Time to prove theorems in the language of Z *)
 
-Open Local Scope IntScope.
+Open Scope IntScope.
 
-Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n.
+Theorem pred_succ : forall n, Z.pred (Z.succ n) == n.
 Proof.
-unfold NZpred, NZsucc, Zeq; intro n; simpl.
-rewrite add_succ_l; now rewrite add_succ_r.
+unfold Z.pred, Z.succ, Z.eq; intro n; simpl; now nzsimpl.
 Qed.
 
-Theorem NZadd_0_l : forall n : Z, 0 + n == n.
+Theorem succ_pred : forall n, Z.succ (Z.pred n) == n.
 Proof.
-intro n; unfold NZadd, Zeq; simpl. now do 2 rewrite add_0_l.
+intro n; unfold Z.succ, Z.pred, Z.eq; simpl; now nzsimpl.
 Qed.
 
-Theorem NZadd_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m).
+Theorem opp_0 : - 0 == 0.
 Proof.
-intros n m; unfold NZadd, Zeq; simpl. now do 2 rewrite add_succ_l.
+unfold Z.opp, Z.eq; simpl. now nzsimpl.
 Qed.
 
-Theorem NZsub_0_r : forall n : Z, n - 0 == n.
+Theorem opp_succ : forall n, - (Z.succ n) == Z.pred (- n).
 Proof.
-intro n; unfold NZsub, Zeq; simpl. now do 2 rewrite add_0_r.
+reflexivity.
 Qed.
 
-Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m).
+Theorem add_0_l : forall n, 0 + n == n.
 Proof.
-intros n m; unfold NZsub, Zeq; simpl. symmetry; now rewrite add_succ_r.
+intro n; unfold Z.add, Z.eq; simpl. now nzsimpl.
 Qed.
 
-Theorem NZmul_0_l : forall n : Z, 0 * n == 0.
+Theorem add_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
 Proof.
-intro n; unfold NZmul, Zeq; simpl.
-repeat rewrite mul_0_l. now rewrite add_assoc.
+intros n m; unfold Z.add, Z.eq; simpl. now nzsimpl.
 Qed.
 
-Theorem NZmul_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m.
+Theorem sub_0_r : forall n, n - 0 == n.
 Proof.
-intros n m; unfold NZmul, NZsucc, Zeq; simpl.
-do 2 rewrite mul_succ_l. ring.
+intro n; unfold Z.sub, Z.eq; simpl. now nzsimpl.
 Qed.
 
-End NZAxiomsMod.
-
-Definition NZlt := Zlt.
-Definition NZle := Zle.
-Definition NZmin := Zmin.
-Definition NZmax := Zmax.
-
-Instance NZlt_wd : Proper (Zeq ==> Zeq ==> iff) NZlt.
+Theorem sub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
 Proof.
-unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
-stepr (snd m1 + fst m2) by apply add_comm.
-apply (add_lt_repl_pair (fst n1) (snd n1)); [| assumption].
-stepl (snd m2 + fst n1) by apply add_comm.
-stepr (fst m2 + snd n1) by apply add_comm.
-apply (add_lt_repl_pair (snd n2) (fst n2)).
-now stepl (fst n1 + snd n2) by apply add_comm.
-stepl (fst m2 + snd n2) by apply add_comm. now stepr (fst n2 + snd m2) by apply add_comm.
-stepr (snd n1 + fst n2) by apply add_comm.
-apply (add_lt_repl_pair (fst m1) (snd m1)); [| now symmetry].
-stepl (snd n2 + fst m1) by apply add_comm.
-stepr (fst n2 + snd m1) by apply add_comm.
-apply (add_lt_repl_pair (snd m2) (fst m2)).
-now stepl (fst m1 + snd m2) by apply add_comm.
-stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm.
+intros n m; unfold Z.sub, Z.eq; simpl. symmetry; now rewrite add_succ_r.
 Qed.
 
-Instance NZle_wd : Proper (Zeq ==> Zeq ==> iff) NZle.
+Theorem mul_0_l : forall n, 0 * n == 0.
 Proof.
-unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
-do 2 rewrite lt_eq_cases. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int.
-fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%Int in H2.
-now rewrite H1, H2.
+intros (n1,n2); unfold Z.mul, Z.eq; simpl; now nzsimpl.
 Qed.
 
-Instance NZmin_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmin.
+Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
 Proof.
-intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl.
-destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
-rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)) by
-now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
-stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
-unfold Zeq in H1. rewrite H1. ring.
-rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
-rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)) by
-now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
-stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
-unfold Zeq in H2. rewrite H2. ring.
+intros (n1,n2) (m1,m2); unfold Z.mul, Z.succ, Z.eq; simpl; nzsimpl.
+rewrite <- (add_assoc _ m1), (add_comm m1), (add_assoc _ _ m1).
+now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%Num m2).
 Qed.
 
-Instance NZmax_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmax.
-Proof.
-intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl.
-destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
-rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)) by
-now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
-stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
-unfold Zeq in H2. rewrite H2. ring.
-rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
-rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)) by
-now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
-stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
-unfold Zeq in H1. rewrite H1. ring.
-Qed.
-
-Open Local Scope IntScope.
-
-Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m.
-Proof.
-intros n m; unfold Zlt, Zle, Zeq; simpl. apply lt_eq_cases.
-Qed.
+(** Order *)
 
-Theorem NZlt_irrefl : forall n : Z, ~ (n < n).
+Lemma lt_eq_cases : forall n m, n<=m <-> n<m \/ n==m.
 Proof.
-intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl.
+intros; apply N.lt_eq_cases.
 Qed.
 
-Theorem NZlt_succ_r : forall n m : Z, n < (Zsucc m) <-> n <= m.
+Theorem lt_irrefl : forall n, ~ (n < n).
 Proof.
-intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite add_succ_l; apply lt_succ_r.
+intros; apply N.lt_irrefl.
 Qed.
 
-Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
+Theorem lt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.
 Proof.
-unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_l by assumption. ring.
+intros n m; unfold Z.lt, Z.le, Z.eq; simpl; nzsimpl. apply lt_succ_r.
 Qed.
 
-Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m.
+Theorem min_l : forall n m, n <= m -> Z.min n m == n.
 Proof.
-unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_r by assumption. ring.
+unfold Z.min, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *.
+rewrite min_l by assumption.
+now rewrite <- add_assoc, (add_comm m2).
 Qed.
 
-Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n.
+Theorem min_r : forall n m, m <= n -> Z.min n m == m.
 Proof.
-unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_l by assumption. ring.
+unfold Z.min, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *.
+rewrite min_r by assumption.
+now rewrite add_assoc.
 Qed.
 
-Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m.
+Theorem max_l : forall n m, m <= n -> Z.max n m == n.
 Proof.
-unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_r by assumption. ring.
+unfold Z.max, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *.
+rewrite max_l by assumption.
+now rewrite <- add_assoc, (add_comm m2).
 Qed.
 
-End NZOrdAxiomsMod.
-
-Definition Zopp (n : Z) : Z := (snd n, fst n).
-
-Notation "- x" := (Zopp x) : IntScope.
-
-Instance Zopp_wd : Proper (Zeq ==> Zeq) Zopp.
+Theorem max_r : forall n m, n <= m -> Z.max n m == m.
 Proof.
-unfold Zeq; intros n m H; simpl. symmetry.
-stepl (fst n + snd m) by apply add_comm.
-now stepr (fst m + snd n) by apply add_comm.
+unfold Z.max, Z.le, Z.eq; simpl; intros n m H.
+rewrite max_r by assumption.
+now rewrite add_assoc.
 Qed.
 
-Open Local Scope IntScope.
-
-Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n.
+Theorem lt_nge : forall n m, n < m <-> ~(m<=n).
 Proof.
-intro n; unfold Zsucc, Zpred, Zeq; simpl.
-rewrite add_succ_l; now rewrite add_succ_r.
+intros. apply lt_nge.
 Qed.
 
-Theorem Zopp_0 : - 0 == 0.
+Instance lt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.
 Proof.
-unfold Zopp, Zeq; simpl. now rewrite add_0_l.
+assert (forall n, Proper (Z.eq==>iff) (Z.lt n)).
+ intros (n1,n2). apply proper_sym_impl_iff; auto with *.
+ unfold Z.lt, Z.eq; intros (r1,r2) (s1,s2) Eq H; simpl in *.
+ apply le_lt_add_lt with (r1+r2)%Num (r1+r2)%Num; [apply le_refl; auto with *|].
+ rewrite add_shuffle2, (add_comm s2), Eq.
+ rewrite (add_comm s1 n2), (add_shuffle1 n2), (add_comm n2 r1).
+ now rewrite <- add_lt_mono_r.
+intros n n' Hn m m' Hm.
+rewrite Hm. rewrite 2 lt_nge, 2 lt_eq_cases, Hn; auto with *.
 Qed.
 
-Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n).
-Proof.
-reflexivity.
-Qed.
+Definition t := Z.t.
+Definition eq := Z.eq.
+Definition zero := Z.zero.
+Definition succ := Z.succ.
+Definition pred := Z.pred.
+Definition add := Z.add.
+Definition sub := Z.sub.
+Definition mul := Z.mul.
+Definition opp := Z.opp.
+Definition lt := Z.lt.
+Definition le := Z.le.
+Definition min := Z.min.
+Definition max := Z.max.
 
 End ZPairsAxiomsMod.
 
@@ -403,9 +311,7 @@ and get their properties *)
 Require Import NPeano.
 
 Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod.
-Module Export ZPairsMulOrderPropMod := ZMulOrderPropFunct ZPairsPeanoAxiomsMod.
-
-Open Local Scope IntScope.
+Module Export ZPairsPropMod := ZPropFunct ZPairsPeanoAxiomsMod.
 
 Eval compute in (3, 5) * (4, 6).
 *)
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 823ef149c2..e2be10ad95 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -16,47 +16,37 @@ Require Import ZSig.
 
 Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
 
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with Z.t.
-Open Local Scope IntScope.
-Notation "[ x ]" := (Z.to_Z x) : IntScope.
-Infix "=="  := Z.eq (at level 70) : IntScope.
-Notation "0" := Z.zero : IntScope.
-Infix "+" := Z.add : IntScope.
-Infix "-" := Z.sub : IntScope.
-Infix "*" := Z.mul : IntScope.
-Notation "- x" := (Z.opp x) : IntScope.
+Delimit Scope NumScope with Num.
+Bind Scope NumScope with Z.t.
+Local Open Scope NumScope.
+Notation "[ x ]" := (Z.to_Z x) : NumScope.
+Infix "=="  := Z.eq (at level 70) : NumScope.
+Notation "0" := Z.zero : NumScope.
+Infix "+" := Z.add : NumScope.
+Infix "-" := Z.sub : NumScope.
+Infix "*" := Z.mul : NumScope.
+Notation "- x" := (Z.opp x) : NumScope.
+Infix "<=" := Z.le : NumScope.
+Infix "<" := Z.lt : NumScope.
 
 Hint Rewrite
  Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
- Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec.
+ Z.spec_mul Z.spec_opp Z.spec_of_Z : zspec.
 
-Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec.
+Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec.
 Ltac zcongruence := repeat red; intros; zsimpl; congruence.
 
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
-
-Definition NZ := Z.t.
-Definition NZeq := Z.eq.
-Definition NZ0 := Z.zero.
-Definition NZsucc := Z.succ.
-Definition NZpred := Z.pred.
-Definition NZadd := Z.add.
-Definition NZsub := Z.sub.
-Definition NZmul := Z.mul.
-
-Instance NZeq_equiv : Equivalence Z.eq.
+Instance eq_equiv : Equivalence Z.eq.
 
 Obligation Tactic := zcongruence.
 
-Program Instance NZsucc_wd : Proper (Z.eq ==> Z.eq) NZsucc.
-Program Instance NZpred_wd : Proper (Z.eq ==> Z.eq) NZpred.
-Program Instance NZadd_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZadd.
-Program Instance NZsub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZsub.
-Program Instance NZmul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZmul.
+Program Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ.
+Program Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred.
+Program Instance add_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add.
+Program Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub.
+Program Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul.
 
-Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n.
+Theorem pred_succ : forall n, Z.pred (Z.succ n) == n.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
@@ -107,7 +97,7 @@ intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto.
 subst z'; auto with zarith.
 Qed.
 
-Theorem NZinduction : forall n, A n.
+Theorem bi_induction : forall n, A n.
 Proof.
 intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)).
 apply B_holds.
@@ -116,45 +106,37 @@ Qed.
 
 End Induction.
 
-Theorem NZadd_0_l : forall n, 0 + n == n.
+Theorem add_0_l : forall n, 0 + n == n.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZadd_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
+Theorem add_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZsub_0_r : forall n, n - 0 == n.
+Theorem sub_0_r : forall n, n - 0 == n.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
+Theorem sub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZmul_0_l : forall n, 0 * n == 0.
+Theorem mul_0_l : forall n, 0 * n == 0.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZmul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
+Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
 Proof.
 intros; zsimpl; ring.
 Qed.
 
-End NZAxiomsMod.
-
-Definition NZlt := Z.lt.
-Definition NZle := Z.le.
-Definition NZmin := Z.min.
-Definition NZmax := Z.max.
-
-Infix "<=" := Z.le : IntScope.
-Infix "<" := Z.lt : IntScope.
+(** Order *)
 
 Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z.
 Proof.
@@ -191,85 +173,84 @@ intros x x' Hx y y' Hy.
 rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition.
 Qed.
 
-Instance NZlt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.
+Instance lt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.
 Proof.
 intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition.
 Qed.
 
-Instance NZle_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.le.
-Proof.
-intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition.
-Qed.
-
-Instance NZmin_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.min.
-Proof.
-repeat red; intros; rewrite 2 spec_min; congruence.
-Qed.
-
-Instance NZmax_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.max.
-Proof.
-repeat red; intros; rewrite 2 spec_max; congruence.
-Qed.
-
-Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
 Proof.
 intros.
 unfold Z.eq; rewrite spec_lt, spec_le; omega.
 Qed.
 
-Theorem NZlt_irrefl : forall n, ~ n < n.
+Theorem lt_irrefl : forall n, ~ n < n.
 Proof.
 intros; rewrite spec_lt; auto with zarith.
 Qed.
 
-Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.
+Theorem lt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.
 Proof.
 intros; rewrite spec_lt, spec_le, Z.spec_succ; omega.
 Qed.
 
-Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n.
+Theorem min_l : forall n m, n <= m -> Z.min n m == n.
 Proof.
 intros n m; unfold Z.eq; rewrite spec_le, spec_min.
 generalize (Zmin_spec [n] [m]); omega.
 Qed.
 
-Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m.
+Theorem min_r : forall n m, m <= n -> Z.min n m == m.
 Proof.
 intros n m; unfold Z.eq; rewrite spec_le, spec_min.
 generalize (Zmin_spec [n] [m]); omega.
 Qed.
 
-Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n.
+Theorem max_l : forall n m, m <= n -> Z.max n m == n.
 Proof.
 intros n m; unfold Z.eq; rewrite spec_le, spec_max.
 generalize (Zmax_spec [n] [m]); omega.
 Qed.
 
-Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m.
+Theorem max_r : forall n m, n <= m -> Z.max n m == m.
 Proof.
 intros n m; unfold Z.eq; rewrite spec_le, spec_max.
 generalize (Zmax_spec [n] [m]); omega.
 Qed.
 
-End NZOrdAxiomsMod.
-
-Definition Zopp := Z.opp.
+(** Part specific to integers, not natural numbers *)
 
-Program Instance Zopp_wd : Proper (Z.eq ==> Z.eq) Z.opp.
+Program Instance opp_wd : Proper (Z.eq ==> Z.eq) Z.opp.
 
-Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n.
+Theorem succ_pred : forall n, Z.succ (Z.pred n) == n.
 Proof.
 red; intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem Zopp_0 : - 0 == 0.
+Theorem opp_0 : - 0 == 0.
 Proof.
 red; intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n).
+Theorem opp_succ : forall n, - (Z.succ n) == Z.pred (- n).
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
+(** Aliases *)
+
+Definition t := Z.t.
+Definition eq := Z.eq.
+Definition zero := Z.zero.
+Definition succ := Z.succ.
+Definition pred := Z.pred.
+Definition add := Z.add.
+Definition sub := Z.sub.
+Definition mul := Z.mul.
+Definition opp := Z.opp.
+Definition lt := Z.lt.
+Definition le := Z.le.
+Definition min := Z.min.
+Definition max := Z.max.
+
 End ZSig_ZAxioms.