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

9 files changed, 511 insertions, 1199 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.