13 files changed, 2637 insertions, 1221 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index df941d90..5663408d 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -8,338 +8,286 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id$ i*)
 
 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.
 
-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 101ea634..de12993f 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -8,365 +8,292 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZAddOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id$ i*)
 
 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.
 
-(* 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 : predicate_wd Zeq P.
-
-Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed.
+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 c4a4b6b8..9158a214 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -8,58 +8,31 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export NZAxioms.
 
 Set Implicit Arguments.
 
-Module Type ZAxiomsSig.
-Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig.
+Module Type Opp (Import T:Typ).
+ Parameter Inline opp : t -> t.
+End Opp.
 
-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.
+Module Type OppNotation (T:Typ)(Import O : Opp T).
+ Notation "- x" := (opp x) (at level 35, right associativity).
+End OppNotation.
 
-Parameter Zopp : Z -> Z.
+Module Type Opp' (T:Typ) := Opp T <+ OppNotation T.
 
-(*Notation "- 1" := (Zopp 1) : IntScope.
-Check (-1).*)
+(** We obtain integers by postulating that every number has a predecessor. *)
 
-Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
+Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z).
+ Declare Instance opp_wd : Proper (eq==>eq) opp.
+ Axiom succ_pred : forall n, S (P n) == n.
+ Axiom opp_0 : - 0 == 0.
+ Axiom opp_succ : forall n, - (S n) == P (- n).
+End IsOpp.
 
-Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
-Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope.
-
-Open Local Scope IntScope.
-
-(* 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).
-
-End ZAxiomsSig.
+Module Type ZAxiomsSig := NZOrdAxiomsSig <+ Opp <+ IsOpp.
+Module Type ZAxiomsSig' := NZOrdAxiomsSig' <+ Opp' <+ IsOpp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 0f71f2cc..44bb02ec 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -8,78 +8,25 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
+(*i $Id$ i*)
 
 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 (proj1 NZeq_equiv).
-
-Theorem Zeq_sym : forall n m : Z, n == m -> m == n.
-Proof (proj2 (proj2 NZeq_equiv)).
-
-Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p.
-Proof (proj1 (proj2 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, predicate_wd Zeq 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.
 
 (* 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/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
new file mode 100644
index 00000000..bcd16fec
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -0,0 +1,605 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** * Euclidean Division for integers, Euclid convention
+
+    We use here the "usual" formulation of the Euclid Theorem
+    [forall a b, b<>0 -> exists b q, a = b*q+r /\ 0 < r < |b| ]
+
+    The outcome of the modulo function is hence always positive.
+    This corresponds to convention "E" in the following paper:
+
+    R. Boute, "The Euclidean definition of the functions div and mod",
+    ACM Transactions on Programming Languages and Systems,
+    Vol. 14, No.2, pp. 127-144, April 1992.
+
+    See files [ZDivTrunc] and [ZDivFloor] for others conventions.
+*)
+
+Require Import ZAxioms ZProperties NZDiv.
+
+Module Type ZDivSpecific (Import Z : ZAxiomsExtSig')(Import DM : DivMod' Z).
+ Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b.
+End ZDivSpecific.
+
+Module Type ZDiv (Z:ZAxiomsExtSig)
+ := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
+
+Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation.
+
+Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
+
+(** We benefit from what already exists for NZ *)
+
+ Module ZD <: NZDiv Z.
+  Definition div := div.
+  Definition modulo := modulo.
+  Definition div_wd := div_wd.
+  Definition mod_wd := mod_wd.
+  Definition div_mod := div_mod.
+  Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
+  Proof.
+  intros. rewrite <- (abs_eq b) at 3 by now apply lt_le_incl.
+  apply mod_always_pos.
+  Qed.
+ End ZD.
+ Module Import NZDivP := NZDivPropFunct Z ZP ZD.
+
+(** Another formulation of the main equation *)
+
+Lemma mod_eq :
+ forall a b, b~=0 -> a mod b == a - b*(a/b).
+Proof.
+intros.
+rewrite <- add_move_l.
+symmetry. now apply div_mod.
+Qed.
+
+Ltac pos_or_neg a :=
+ let LT := fresh "LT" in
+ let LE := fresh "LE" in
+ destruct (le_gt_cases 0 a) as [LE|LT]; [|rewrite <- opp_pos_neg in LT].
+
+(** Uniqueness theorems *)
+
+Theorem div_mod_unique : forall b q1 q2 r1 r2 : t,
+  0<=r1<abs b -> 0<=r2<abs b ->
+  b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2.
+Proof.
+intros b q1 q2 r1 r2 Hr1 Hr2 EQ.
+pos_or_neg b.
+rewrite abs_eq in * by trivial.
+apply div_mod_unique with b; trivial.
+rewrite abs_neq' in * by auto using lt_le_incl.
+rewrite eq_sym_iff. apply div_mod_unique with (-b); trivial.
+rewrite 2 mul_opp_l.
+rewrite add_move_l, sub_opp_r.
+rewrite <-add_assoc.
+symmetry. rewrite add_move_l, sub_opp_r.
+now rewrite (add_comm r2), (add_comm r1).
+Qed.
+
+Theorem div_unique:
+ forall a b q r, 0<=r<abs b -> a == b*q + r -> q == a/b.
+Proof.
+intros a b q r Hr EQ.
+assert (Hb : b~=0).
+ pos_or_neg b.
+ rewrite abs_eq in Hr; intuition; order.
+ rewrite <- opp_0, eq_opp_r. rewrite abs_neq' in Hr; intuition; order.
+destruct (div_mod_unique b q (a/b) r (a mod b)); trivial.
+now apply mod_always_pos.
+now rewrite <- div_mod.
+Qed.
+
+Theorem mod_unique:
+ forall a b q r, 0<=r<abs b -> a == b*q + r -> r == a mod b.
+Proof.
+intros a b q r Hr EQ.
+assert (Hb : b~=0).
+ pos_or_neg b.
+ rewrite abs_eq in Hr; intuition; order.
+ rewrite <- opp_0, eq_opp_r. rewrite abs_neq' in Hr; intuition; order.
+destruct (div_mod_unique b q (a/b) r (a mod b)); trivial.
+now apply mod_always_pos.
+now rewrite <- div_mod.
+Qed.
+
+(** Sign rules *)
+
+Lemma div_opp_r : forall a b, b~=0 -> a/(-b) == -(a/b).
+Proof.
+intros. symmetry.
+apply div_unique with (a mod b).
+rewrite abs_opp; apply mod_always_pos.
+rewrite mul_opp_opp; now apply div_mod.
+Qed.
+
+Lemma mod_opp_r : forall a b, b~=0 -> a mod (-b) == a mod b.
+Proof.
+intros. symmetry.
+apply mod_unique with (-(a/b)).
+rewrite abs_opp; apply mod_always_pos.
+rewrite mul_opp_opp; now apply div_mod.
+Qed.
+
+Lemma div_opp_l_z : forall a b, b~=0 -> a mod b == 0 ->
+ (-a)/b == -(a/b).
+Proof.
+intros a b Hb Hab. symmetry.
+apply div_unique with (-(a mod b)).
+rewrite Hab, opp_0. split; [order|].
+pos_or_neg b; [rewrite abs_eq | rewrite abs_neq']; order.
+now rewrite mul_opp_r, <-opp_add_distr, <-div_mod.
+Qed.
+
+Lemma div_opp_l_nz : forall a b, b~=0 -> a mod b ~= 0 ->
+ (-a)/b == -(a/b)-sgn b.
+Proof.
+intros a b Hb Hab. symmetry.
+apply div_unique with (abs b -(a mod b)).
+rewrite lt_sub_lt_add_l.
+rewrite <- le_add_le_sub_l. nzsimpl.
+rewrite <- (add_0_l (abs b)) at 2.
+rewrite <- add_lt_mono_r.
+destruct (mod_always_pos a b); intuition order.
+rewrite <- 2 add_opp_r, mul_add_distr_l, 2 mul_opp_r.
+rewrite sgn_abs.
+rewrite add_shuffle2, add_opp_diag_l; nzsimpl.
+rewrite <-opp_add_distr, <-div_mod; order.
+Qed.
+
+Lemma mod_opp_l_z : forall a b, b~=0 -> a mod b == 0 ->
+ (-a) mod b == 0.
+Proof.
+intros a b Hb Hab. symmetry.
+apply mod_unique with (-(a/b)).
+split; [order|now rewrite abs_pos].
+now rewrite <-opp_0, <-Hab, mul_opp_r, <-opp_add_distr, <-div_mod.
+Qed.
+
+Lemma mod_opp_l_nz : forall a b, b~=0 -> a mod b ~= 0 ->
+ (-a) mod b == abs b - (a mod b).
+Proof.
+intros a b Hb Hab. symmetry.
+apply mod_unique with (-(a/b)-sgn b).
+rewrite lt_sub_lt_add_l.
+rewrite <- le_add_le_sub_l. nzsimpl.
+rewrite <- (add_0_l (abs b)) at 2.
+rewrite <- add_lt_mono_r.
+destruct (mod_always_pos a b); intuition order.
+rewrite <- 2 add_opp_r, mul_add_distr_l, 2 mul_opp_r.
+rewrite sgn_abs.
+rewrite add_shuffle2, add_opp_diag_l; nzsimpl.
+rewrite <-opp_add_distr, <-div_mod; order.
+Qed.
+
+Lemma div_opp_opp_z : forall a b, b~=0 -> a mod b == 0 ->
+ (-a)/(-b) == a/b.
+Proof.
+intros. now rewrite div_opp_r, div_opp_l_z, opp_involutive.
+Qed.
+
+Lemma div_opp_opp_nz : forall a b, b~=0 -> a mod b ~= 0 ->
+ (-a)/(-b) == a/b + sgn(b).
+Proof.
+intros. rewrite div_opp_r, div_opp_l_nz by trivial.
+now rewrite opp_sub_distr, opp_involutive.
+Qed.
+
+Lemma mod_opp_opp_z : forall a b, b~=0 -> a mod b == 0 ->
+ (-a) mod (-b) == 0.
+Proof.
+intros. now rewrite mod_opp_r, mod_opp_l_z.
+Qed.
+
+Lemma mod_opp_opp_nz : forall a b, b~=0 -> a mod b ~= 0 ->
+ (-a) mod (-b) == abs b - a mod b.
+Proof.
+intros. now rewrite mod_opp_r, mod_opp_l_nz.
+Qed.
+
+(** A division by itself returns 1 *)
+
+Lemma div_same : forall a, a~=0 -> a/a == 1.
+Proof.
+intros. symmetry. apply div_unique with 0.
+split; [order|now rewrite abs_pos].
+now nzsimpl.
+Qed.
+
+Lemma mod_same : forall a, a~=0 -> a mod a == 0.
+Proof.
+intros.
+rewrite mod_eq, div_same by trivial. nzsimpl. apply sub_diag.
+Qed.
+
+(** A division of a small number by a bigger one yields zero. *)
+
+Theorem div_small: forall a b, 0<=a<b -> a/b == 0.
+Proof. exact div_small. Qed.
+
+(** Same situation, in term of modulo: *)
+
+Theorem mod_small: forall a b, 0<=a<b -> a mod b == a.
+Proof. exact mod_small. Qed.
+
+(** * Basic values of divisions and modulo. *)
+
+Lemma div_0_l: forall a, a~=0 -> 0/a == 0.
+Proof.
+intros. pos_or_neg a. apply div_0_l; order.
+apply opp_inj. rewrite <- div_opp_r, opp_0 by trivial. now apply div_0_l.
+Qed.
+
+Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0.
+Proof.
+intros; rewrite mod_eq, div_0_l; now nzsimpl.
+Qed.
+
+Lemma div_1_r: forall a, a/1 == a.
+Proof.
+intros. symmetry. apply div_unique with 0.
+assert (H:=lt_0_1); rewrite abs_pos; intuition; order.
+now nzsimpl.
+Qed.
+
+Lemma mod_1_r: forall a, a mod 1 == 0.
+Proof.
+intros. rewrite mod_eq, div_1_r; nzsimpl; auto using sub_diag.
+apply neq_sym, lt_neq; apply lt_0_1.
+Qed.
+
+Lemma div_1_l: forall a, 1<a -> 1/a == 0.
+Proof. exact div_1_l. Qed.
+
+Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
+Proof. exact mod_1_l. Qed.
+
+Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a.
+Proof.
+intros. symmetry. apply div_unique with 0.
+split; [order|now rewrite abs_pos].
+nzsimpl; apply mul_comm.
+Qed.
+
+Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0.
+Proof.
+intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
+Qed.
+
+(** * Order results about mod and div *)
+
+(** A modulo cannot grow beyond its starting point. *)
+
+Theorem mod_le: forall a b, 0<=a -> b~=0 -> a mod b <= a.
+Proof.
+intros. pos_or_neg b. apply mod_le; order.
+rewrite <- mod_opp_r by trivial. apply mod_le; order.
+Qed.
+
+Theorem div_pos : forall a b, 0<=a -> 0<b -> 0<= a/b.
+Proof. exact div_pos. Qed.
+
+Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.
+Proof. exact div_str_pos. Qed.
+
+Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> 0<=a<abs b).
+Proof.
+intros a b Hb.
+split.
+intros EQ.
+rewrite (div_mod a b Hb), EQ; nzsimpl.
+apply mod_always_pos.
+intros. pos_or_neg b.
+apply div_small.
+now rewrite <- (abs_eq b).
+apply opp_inj; rewrite opp_0, <- div_opp_r by trivial.
+apply div_small.
+rewrite <- (abs_neq' b) by order. trivial.
+Qed.
+
+Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> 0<=a<abs b).
+Proof.
+intros.
+rewrite <- div_small_iff, mod_eq by trivial.
+rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l.
+rewrite eq_sym_iff, eq_mul_0. tauto.
+Qed.
+
+(** As soon as the divisor is strictly greater than 1,
+    the division is strictly decreasing. *)
+
+Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a.
+Proof. exact div_lt. Qed.
+
+(** [le] is compatible with a positive division. *)
+
+Lemma div_le_mono : forall a b c, 0<c -> a<=b -> a/c <= b/c.
+Proof.
+intros a b c Hc Hab.
+rewrite lt_eq_cases in Hab. destruct Hab as [LT|EQ];
+ [|rewrite EQ; order].
+rewrite <- lt_succ_r.
+rewrite (mul_lt_mono_pos_l c) by order.
+nzsimpl.
+rewrite (add_lt_mono_r _ _ (a mod c)).
+rewrite <- div_mod by order.
+apply lt_le_trans with b; trivial.
+rewrite (div_mod b c) at 1 by order.
+rewrite <- add_assoc, <- add_le_mono_l.
+apply le_trans with (c+0).
+nzsimpl; destruct (mod_always_pos b c); try order.
+rewrite abs_eq in *; order.
+rewrite <- add_le_mono_l. destruct (mod_always_pos a c); order.
+Qed.
+
+(** In this convention, [div] performs Rounding-Toward-Bottom
+    when divisor is positive, and Rounding-Toward-Top otherwise.
+
+    Since we cannot speak of rational values here, we express this
+    fact by multiplying back by [b], and this leads to a nice
+    unique statement.
+*)
+
+Lemma mul_div_le : forall a b, b~=0 -> b*(a/b) <= a.
+Proof.
+intros.
+rewrite (div_mod a b) at 2; trivial.
+rewrite <- (add_0_r (b*(a/b))) at 1.
+rewrite <- add_le_mono_l.
+now destruct (mod_always_pos a b).
+Qed.
+
+(** Giving a reversed bound is slightly more complex *)
+
+Lemma mul_succ_div_gt: forall a b, 0<b -> a < b*(S (a/b)).
+Proof.
+intros.
+nzsimpl.
+rewrite (div_mod a b) at 1; try order.
+rewrite <- add_lt_mono_l.
+destruct (mod_always_pos a b).
+rewrite abs_eq in *; order.
+Qed.
+
+Lemma mul_pred_div_gt: forall a b, b<0 -> a < b*(P (a/b)).
+Proof.
+intros a b Hb.
+rewrite mul_pred_r, <- add_opp_r.
+rewrite (div_mod a b) at 1; try order.
+rewrite <- add_lt_mono_l.
+destruct (mod_always_pos a b).
+rewrite <- opp_pos_neg in Hb. rewrite abs_neq' in *; order.
+Qed.
+
+(** NB: The three previous properties could be used as
+    specifications for [div]. *)
+
+(** Inequality [mul_div_le] is exact iff the modulo is zero. *)
+
+Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).
+Proof.
+intros.
+rewrite (div_mod a b) at 1; try order.
+rewrite <- (add_0_r (b*(a/b))) at 2.
+apply add_cancel_l.
+Qed.
+
+(** Some additionnal inequalities about div. *)
+
+Theorem div_lt_upper_bound:
+  forall a b q, 0<b -> a < b*q -> a/b < q.
+Proof.
+intros.
+rewrite (mul_lt_mono_pos_l b) by trivial.
+apply le_lt_trans with a; trivial.
+apply mul_div_le; order.
+Qed.
+
+Theorem div_le_upper_bound:
+  forall a b q, 0<b -> a <= b*q -> a/b <= q.
+Proof.
+intros.
+rewrite <- (div_mul q b) by order.
+apply div_le_mono; trivial. now rewrite mul_comm.
+Qed.
+
+Theorem div_le_lower_bound:
+  forall a b q, 0<b -> b*q <= a -> q <= a/b.
+Proof.
+intros.
+rewrite <- (div_mul q b) by order.
+apply div_le_mono; trivial. now rewrite mul_comm.
+Qed.
+
+(** A division respects opposite monotonicity for the divisor *)
+
+Lemma div_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p/r <= p/q.
+Proof. exact div_le_compat_l. Qed.
+
+(** * Relations between usual operations and mod and div *)
+
+Lemma mod_add : forall a b c, c~=0 ->
+ (a + b * c) mod c == a mod c.
+Proof.
+intros.
+symmetry.
+apply mod_unique with (a/c+b); trivial.
+now apply mod_always_pos.
+rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
+now rewrite mul_comm.
+Qed.
+
+Lemma div_add : forall a b c, c~=0 ->
+ (a + b * c) / c == a / c + b.
+Proof.
+intros.
+apply (mul_cancel_l _ _ c); try order.
+apply (add_cancel_r _ _ ((a+b*c) mod c)).
+rewrite <- div_mod, mod_add by order.
+rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
+now rewrite mul_comm.
+Qed.
+
+Lemma div_add_l: forall a b c, b~=0 ->
+ (a * b + c) / b == a + c / b.
+Proof.
+ intros a b c. rewrite (add_comm _ c), (add_comm a).
+ now apply div_add.
+Qed.
+
+(** Cancellations. *)
+
+(** With the current convention, the following isn't always true
+    when [c<0]: [-3*-1 / -2*-1 = 3/2 = 1] while [-3/-2 = 2] *)
+
+Lemma div_mul_cancel_r : forall a b c, b~=0 -> 0<c ->
+ (a*c)/(b*c) == a/b.
+Proof.
+intros.
+symmetry.
+apply div_unique with ((a mod b)*c).
+(* ineqs *)
+rewrite abs_mul, (abs_eq c) by order.
+rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial.
+apply mod_always_pos.
+(* equation *)
+rewrite (div_mod a b) at 1 by order.
+rewrite mul_add_distr_r.
+rewrite add_cancel_r.
+rewrite <- 2 mul_assoc. now rewrite (mul_comm c).
+Qed.
+
+Lemma div_mul_cancel_l : forall a b c, b~=0 -> 0<c ->
+ (c*a)/(c*b) == a/b.
+Proof.
+intros. rewrite !(mul_comm c); now apply div_mul_cancel_r.
+Qed.
+
+Lemma mul_mod_distr_l: forall a b c, b~=0 -> 0<c ->
+  (c*a) mod (c*b) == c * (a mod b).
+Proof.
+intros.
+rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))).
+rewrite <- div_mod.
+rewrite div_mul_cancel_l by trivial.
+rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
+apply div_mod; order.
+rewrite <- neq_mul_0; intuition; order.
+Qed.
+
+Lemma mul_mod_distr_r: forall a b c, b~=0 -> 0<c ->
+  (a*c) mod (b*c) == (a mod b) * c.
+Proof.
+ intros. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l.
+Qed.
+
+
+(** Operations modulo. *)
+
+Theorem mod_mod: forall a n, n~=0 ->
+ (a mod n) mod n == a mod n.
+Proof.
+intros. rewrite mod_small_iff by trivial.
+now apply mod_always_pos.
+Qed.
+
+Lemma mul_mod_idemp_l : forall a b n, n~=0 ->
+ ((a mod n)*b) mod n == (a*b) mod n.
+Proof.
+ intros a b n Hn. symmetry.
+ rewrite (div_mod a n) at 1 by order.
+ rewrite add_comm, (mul_comm n), (mul_comm _ b).
+ rewrite mul_add_distr_l, mul_assoc.
+ rewrite mod_add by trivial.
+ now rewrite mul_comm.
+Qed.
+
+Lemma mul_mod_idemp_r : forall a b n, n~=0 ->
+ (a*(b mod n)) mod n == (a*b) mod n.
+Proof.
+ intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l.
+Qed.
+
+Theorem mul_mod: forall a b n, n~=0 ->
+ (a * b) mod n == ((a mod n) * (b mod n)) mod n.
+Proof.
+ intros. now rewrite mul_mod_idemp_l, mul_mod_idemp_r.
+Qed.
+
+Lemma add_mod_idemp_l : forall a b n, n~=0 ->
+ ((a mod n)+b) mod n == (a+b) mod n.
+Proof.
+ intros a b n Hn. symmetry.
+ rewrite (div_mod a n) at 1 by order.
+ rewrite <- add_assoc, add_comm, mul_comm.
+ now rewrite mod_add.
+Qed.
+
+Lemma add_mod_idemp_r : forall a b n, n~=0 ->
+ (a+(b mod n)) mod n == (a+b) mod n.
+Proof.
+ intros. rewrite !(add_comm a). now apply add_mod_idemp_l.
+Qed.
+
+Theorem add_mod: forall a b n, n~=0 ->
+ (a+b) mod n == (a mod n + b mod n) mod n.
+Proof.
+ intros. now rewrite add_mod_idemp_l, add_mod_idemp_r.
+Qed.
+
+(** With the current convention, the following result isn't always
+    true for negative divisors. For instance
+    [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ]. *)
+
+Lemma div_div : forall a b c, 0<b -> 0<c ->
+ (a/b)/c == a/(b*c).
+Proof.
+ intros a b c Hb Hc.
+ apply div_unique with (b*((a/b) mod c) + a mod b).
+ (* begin 0<= ... <abs(b*c) *)
+ rewrite abs_mul.
+ destruct (mod_always_pos (a/b) c), (mod_always_pos a b).
+ split.
+ apply add_nonneg_nonneg; trivial.
+ apply mul_nonneg_nonneg; order.
+ apply lt_le_trans with (b*((a/b) mod c) + abs b).
+ now rewrite <- add_lt_mono_l.
+ rewrite (abs_eq b) by order.
+ now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l.
+ (* end 0<= ... < abs(b*c) *)
+ rewrite (div_mod a b) at 1 by order.
+ rewrite add_assoc, add_cancel_r.
+ rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
+ apply div_mod; order.
+Qed.
+
+(** A last inequality: *)
+
+Theorem div_mul_le:
+ forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b.
+Proof. exact div_mul_le. Qed.
+
+(** mod is related to divisibility *)
+
+Lemma mod_divides : forall a b, b~=0 ->
+ (a mod b == 0 <-> exists c, a == b*c).
+Proof.
+intros a b Hb. split.
+intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1.
+ rewrite Hab; now nzsimpl.
+intros (c,Hc).
+rewrite Hc, mul_comm.
+now apply mod_mul.
+Qed.
+
+
+End ZDivPropFunct.
+
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
new file mode 100644
index 00000000..1e7624ba
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -0,0 +1,632 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** * Euclidean Division for integers (Floor convention)
+
+    We use here the convention known as Floor, or Round-Toward-Bottom,
+    where [a/b] is the closest integer below the exact fraction.
+    It can be summarized by:
+
+    [a = bq+r /\ 0 <= |r| < |b| /\ Sign(r) = Sign(b)]
+
+    This is the convention followed historically by [Zdiv] in Coq, and
+    corresponds to convention "F" in the following paper:
+
+    R. Boute, "The Euclidean definition of the functions div and mod",
+    ACM Transactions on Programming Languages and Systems,
+    Vol. 14, No.2, pp. 127-144, April 1992.
+
+    See files [ZDivTrunc] and [ZDivEucl] for others conventions.
+*)
+
+Require Import ZAxioms ZProperties NZDiv.
+
+Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z).
+ Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b.
+ Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0.
+End ZDivSpecific.
+
+Module Type ZDiv (Z:ZAxiomsSig)
+ := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
+
+Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation.
+
+Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
+
+(** We benefit from what already exists for NZ *)
+
+ Module ZD <: NZDiv Z.
+  Definition div := div.
+  Definition modulo := modulo.
+  Definition div_wd := div_wd.
+  Definition mod_wd := mod_wd.
+  Definition div_mod := div_mod.
+  Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
+  Proof. intros. now apply mod_pos_bound. Qed.
+ End ZD.
+ Module Import NZDivP := NZDivPropFunct Z ZP ZD.
+
+(** Another formulation of the main equation *)
+
+Lemma mod_eq :
+ forall a b, b~=0 -> a mod b == a - b*(a/b).
+Proof.
+intros.
+rewrite <- add_move_l.
+symmetry. now apply div_mod.
+Qed.
+
+(** Uniqueness theorems *)
+
+Theorem div_mod_unique : forall b q1 q2 r1 r2 : t,
+  (0<=r1<b \/ b<r1<=0) -> (0<=r2<b \/ b<r2<=0) ->
+  b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2.
+Proof.
+intros b q1 q2 r1 r2 Hr1 Hr2 EQ.
+destruct Hr1; destruct Hr2; try (intuition; order).
+apply div_mod_unique with b; trivial.
+rewrite <- (opp_inj_wd r1 r2).
+apply div_mod_unique with (-b); trivial.
+rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.
+rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.
+now rewrite 2 mul_opp_l, <- 2 opp_add_distr, opp_inj_wd.
+Qed.
+
+Theorem div_unique:
+ forall a b q r, (0<=r<b \/ b<r<=0) -> a == b*q + r -> q == a/b.
+Proof.
+intros a b q r Hr EQ.
+assert (Hb : b~=0) by (destruct Hr; intuition; order).
+destruct (div_mod_unique b q (a/b) r (a mod b)); trivial.
+destruct Hr; [left; apply mod_pos_bound|right; apply mod_neg_bound];
+ intuition order.
+now rewrite <- div_mod.
+Qed.
+
+Theorem div_unique_pos:
+ forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b.
+Proof. intros; apply div_unique with r; auto. Qed.
+
+Theorem div_unique_neg:
+ forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b.
+Proof. intros; apply div_unique with r; auto. Qed.
+
+Theorem mod_unique:
+ forall a b q r, (0<=r<b \/ b<r<=0) -> a == b*q + r -> r == a mod b.
+Proof.
+intros a b q r Hr EQ.
+assert (Hb : b~=0) by (destruct Hr; intuition; order).
+destruct (div_mod_unique b q (a/b) r (a mod b)); trivial.
+destruct Hr; [left; apply mod_pos_bound|right; apply mod_neg_bound];
+ intuition order.
+now rewrite <- div_mod.
+Qed.
+
+Theorem mod_unique_pos:
+ forall a b q r, 0<=r<b -> a == b*q + r -> r == a mod b.
+Proof. intros; apply mod_unique with q; auto. Qed.
+
+Theorem mod_unique_neg:
+ forall a b q r, b<r<=0 -> a == b*q + r -> r == a mod b.
+Proof. intros; apply mod_unique with q; auto. Qed.
+
+(** Sign rules *)
+
+Ltac pos_or_neg a :=
+ let LT := fresh "LT" in
+ let LE := fresh "LE" in
+ destruct (le_gt_cases 0 a) as [LE|LT]; [|rewrite <- opp_pos_neg in LT].
+
+Fact mod_bound_or : forall a b, b~=0 -> 0<=a mod b<b \/ b<a mod b<=0.
+Proof.
+intros.
+destruct (lt_ge_cases 0 b); [left|right].
+ apply mod_pos_bound; trivial. apply mod_neg_bound; order.
+Qed.
+
+Fact opp_mod_bound_or : forall a b, b~=0 ->
+ 0 <= -(a mod b) < -b \/ -b < -(a mod b) <= 0.
+Proof.
+intros.
+destruct (lt_ge_cases 0 b); [right|left].
+rewrite <- opp_lt_mono, opp_nonpos_nonneg.
+ destruct (mod_pos_bound a b); intuition; order.
+rewrite <- opp_lt_mono, opp_nonneg_nonpos.
+ destruct (mod_neg_bound a b); intuition; order.
+Qed.
+
+Lemma div_opp_opp : forall a b, b~=0 -> -a/-b == a/b.
+Proof.
+intros. symmetry. apply div_unique with (- (a mod b)).
+now apply opp_mod_bound_or.
+rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order.
+Qed.
+
+Lemma mod_opp_opp : forall a b, b~=0 -> (-a) mod (-b) == - (a mod b).
+Proof.
+intros. symmetry. apply mod_unique with (a/b).
+now apply opp_mod_bound_or.
+rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order.
+Qed.
+
+(** With the current conventions, the other sign rules are rather complex. *)
+
+Lemma div_opp_l_z :
+ forall a b, b~=0 -> a mod b == 0 -> (-a)/b == -(a/b).
+Proof.
+intros a b Hb H. symmetry. apply div_unique with 0.
+destruct (lt_ge_cases 0 b); [left|right]; intuition; order.
+rewrite <- opp_0, <- H.
+rewrite mul_opp_r, <- opp_add_distr, <- div_mod; order.
+Qed.
+
+Lemma div_opp_l_nz :
+ forall a b, b~=0 -> a mod b ~= 0 -> (-a)/b == -(a/b)-1.
+Proof.
+intros a b Hb H. symmetry. apply div_unique with (b - a mod b).
+destruct (lt_ge_cases 0 b); [left|right].
+rewrite le_0_sub. rewrite <- (sub_0_r b) at 5. rewrite <- sub_lt_mono_l.
+destruct (mod_pos_bound a b); intuition; order.
+rewrite le_sub_0. rewrite <- (sub_0_r b) at 1. rewrite <- sub_lt_mono_l.
+destruct (mod_neg_bound a b); intuition; order.
+rewrite <- (add_opp_r b), mul_sub_distr_l, mul_1_r, sub_add_simpl_r_l.
+rewrite mul_opp_r, <-opp_add_distr, <-div_mod; order.
+Qed.
+
+Lemma mod_opp_l_z :
+ forall a b, b~=0 -> a mod b == 0 -> (-a) mod b == 0.
+Proof.
+intros a b Hb H. symmetry. apply mod_unique with (-(a/b)).
+destruct (lt_ge_cases 0 b); [left|right]; intuition; order.
+rewrite <- opp_0, <- H.
+rewrite mul_opp_r, <- opp_add_distr, <- div_mod; order.
+Qed.
+
+Lemma mod_opp_l_nz :
+ forall a b, b~=0 -> a mod b ~= 0 -> (-a) mod b == b - a mod b.
+Proof.
+intros a b Hb H. symmetry. apply mod_unique with (-(a/b)-1).
+destruct (lt_ge_cases 0 b); [left|right].
+rewrite le_0_sub. rewrite <- (sub_0_r b) at 5. rewrite <- sub_lt_mono_l.
+destruct (mod_pos_bound a b); intuition; order.
+rewrite le_sub_0. rewrite <- (sub_0_r b) at 1. rewrite <- sub_lt_mono_l.
+destruct (mod_neg_bound a b); intuition; order.
+rewrite <- (add_opp_r b), mul_sub_distr_l, mul_1_r, sub_add_simpl_r_l.
+rewrite mul_opp_r, <-opp_add_distr, <-div_mod; order.
+Qed.
+
+Lemma div_opp_r_z :
+ forall a b, b~=0 -> a mod b == 0 -> a/(-b) == -(a/b).
+Proof.
+intros. rewrite <- (opp_involutive a) at 1.
+rewrite div_opp_opp; auto using div_opp_l_z.
+Qed.
+
+Lemma div_opp_r_nz :
+ forall a b, b~=0 -> a mod b ~= 0 -> a/(-b) == -(a/b)-1.
+Proof.
+intros. rewrite <- (opp_involutive a) at 1.
+rewrite div_opp_opp; auto using div_opp_l_nz.
+Qed.
+
+Lemma mod_opp_r_z :
+ forall a b, b~=0 -> a mod b == 0 -> a mod (-b) == 0.
+Proof.
+intros. rewrite <- (opp_involutive a) at 1.
+now rewrite mod_opp_opp, mod_opp_l_z, opp_0.
+Qed.
+
+Lemma mod_opp_r_nz :
+ forall a b, b~=0 -> a mod b ~= 0 -> a mod (-b) == (a mod b) - b.
+Proof.
+intros. rewrite <- (opp_involutive a) at 1.
+rewrite mod_opp_opp, mod_opp_l_nz by trivial.
+now rewrite opp_sub_distr, add_comm, add_opp_r.
+Qed.
+
+(** The sign of [a mod b] is the one of [b] *)
+
+(* TODO: a proper sgn function and theory *)
+
+Lemma mod_sign : forall a b, b~=0 -> (0 <= (a mod b) * b).
+Proof.
+intros. destruct (lt_ge_cases 0 b).
+apply mul_nonneg_nonneg; destruct (mod_pos_bound a b); order.
+apply mul_nonpos_nonpos; destruct (mod_neg_bound a b); order.
+Qed.
+
+(** A division by itself returns 1 *)
+
+Lemma div_same : forall a, a~=0 -> a/a == 1.
+Proof.
+intros. pos_or_neg a. apply div_same; order.
+rewrite <- div_opp_opp by trivial. now apply div_same.
+Qed.
+
+Lemma mod_same : forall a, a~=0 -> a mod a == 0.
+Proof.
+intros. rewrite mod_eq, div_same by trivial. nzsimpl. apply sub_diag.
+Qed.
+
+(** A division of a small number by a bigger one yields zero. *)
+
+Theorem div_small: forall a b, 0<=a<b -> a/b == 0.
+Proof. exact div_small. Qed.
+
+(** Same situation, in term of modulo: *)
+
+Theorem mod_small: forall a b, 0<=a<b -> a mod b == a.
+Proof. exact mod_small. Qed.
+
+(** * Basic values of divisions and modulo. *)
+
+Lemma div_0_l: forall a, a~=0 -> 0/a == 0.
+Proof.
+intros. pos_or_neg a. apply div_0_l; order.
+rewrite <- div_opp_opp, opp_0 by trivial. now apply div_0_l.
+Qed.
+
+Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0.
+Proof.
+intros; rewrite mod_eq, div_0_l; now nzsimpl.
+Qed.
+
+Lemma div_1_r: forall a, a/1 == a.
+Proof.
+intros. symmetry. apply div_unique with 0. left. split; order || apply lt_0_1.
+now nzsimpl.
+Qed.
+
+Lemma mod_1_r: forall a, a mod 1 == 0.
+Proof.
+intros. rewrite mod_eq, div_1_r; nzsimpl; auto using sub_diag.
+intro EQ; symmetry in EQ; revert EQ; apply lt_neq; apply lt_0_1.
+Qed.
+
+Lemma div_1_l: forall a, 1<a -> 1/a == 0.
+Proof. exact div_1_l. Qed.
+
+Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
+Proof. exact mod_1_l. Qed.
+
+Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a.
+Proof.
+intros. symmetry. apply div_unique with 0.
+destruct (lt_ge_cases 0 b); [left|right]; split; order.
+nzsimpl; apply mul_comm.
+Qed.
+
+Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0.
+Proof.
+intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
+Qed.
+
+(** * Order results about mod and div *)
+
+(** A modulo cannot grow beyond its starting point. *)
+
+Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a.
+Proof. exact mod_le. Qed.
+
+Theorem div_pos : forall a b, 0<=a -> 0<b -> 0<= a/b.
+Proof. exact div_pos. Qed.
+
+Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.
+Proof. exact div_str_pos. Qed.
+
+Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> 0<=a<b \/ b<a<=0).
+Proof.
+intros a b Hb.
+split.
+intros EQ.
+rewrite (div_mod a b Hb), EQ; nzsimpl.
+now apply mod_bound_or.
+destruct 1. now apply div_small.
+rewrite <- div_opp_opp by trivial. apply div_small; trivial.
+rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.
+Qed.
+
+Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> 0<=a<b \/ b<a<=0).
+Proof.
+intros.
+rewrite <- div_small_iff, mod_eq by trivial.
+rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l.
+rewrite eq_sym_iff, eq_mul_0. tauto.
+Qed.
+
+(** As soon as the divisor is strictly greater than 1,
+    the division is strictly decreasing. *)
+
+Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a.
+Proof. exact div_lt. Qed.
+
+(** [le] is compatible with a positive division. *)
+
+Lemma div_le_mono : forall a b c, 0<c -> a<=b -> a/c <= b/c.
+Proof.
+intros a b c Hc Hab.
+rewrite lt_eq_cases in Hab. destruct Hab as [LT|EQ];
+ [|rewrite EQ; order].
+rewrite <- lt_succ_r.
+rewrite (mul_lt_mono_pos_l c) by order.
+nzsimpl.
+rewrite (add_lt_mono_r _ _ (a mod c)).
+rewrite <- div_mod by order.
+apply lt_le_trans with b; trivial.
+rewrite (div_mod b c) at 1 by order.
+rewrite <- add_assoc, <- add_le_mono_l.
+apply le_trans with (c+0).
+nzsimpl; destruct (mod_pos_bound b c); order.
+rewrite <- add_le_mono_l. destruct (mod_pos_bound a c); order.
+Qed.
+
+(** In this convention, [div] performs Rounding-Toward-Bottom.
+
+    Since we cannot speak of rational values here, we express this
+    fact by multiplying back by [b], and this leads to separates
+    statements according to the sign of [b].
+
+    First, [a/b] is below the exact fraction ...
+*)
+
+Lemma mul_div_le : forall a b, 0<b -> b*(a/b) <= a.
+Proof.
+intros.
+rewrite (div_mod a b) at 2; try order.
+rewrite <- (add_0_r (b*(a/b))) at 1.
+rewrite <- add_le_mono_l.
+now destruct (mod_pos_bound a b).
+Qed.
+
+Lemma mul_div_ge : forall a b, b<0 -> a <= b*(a/b).
+Proof.
+intros. rewrite <- div_opp_opp, opp_le_mono, <-mul_opp_l by order.
+apply mul_div_le. now rewrite opp_pos_neg.
+Qed.
+
+(** ... and moreover it is the larger such integer, since [S(a/b)]
+    is strictly above the exact fraction.
+*)
+
+Lemma mul_succ_div_gt: forall a b, 0<b -> a < b*(S (a/b)).
+Proof.
+intros.
+nzsimpl.
+rewrite (div_mod a b) at 1; try order.
+rewrite <- add_lt_mono_l.
+destruct (mod_pos_bound a b); order.
+Qed.
+
+Lemma mul_succ_div_lt: forall a b, b<0 -> b*(S (a/b)) < a.
+Proof.
+intros. rewrite <- div_opp_opp, opp_lt_mono, <-mul_opp_l by order.
+apply mul_succ_div_gt. now rewrite opp_pos_neg.
+Qed.
+
+(** NB: The four previous properties could be used as
+    specifications for [div]. *)
+
+(** Inequality [mul_div_le] is exact iff the modulo is zero. *)
+
+Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).
+Proof.
+intros.
+rewrite (div_mod a b) at 1; try order.
+rewrite <- (add_0_r (b*(a/b))) at 2.
+apply add_cancel_l.
+Qed.
+
+(** Some additionnal inequalities about div. *)
+
+Theorem div_lt_upper_bound:
+  forall a b q, 0<b -> a < b*q -> a/b < q.
+Proof.
+intros.
+rewrite (mul_lt_mono_pos_l b) by trivial.
+apply le_lt_trans with a; trivial.
+now apply mul_div_le.
+Qed.
+
+Theorem div_le_upper_bound:
+  forall a b q, 0<b -> a <= b*q -> a/b <= q.
+Proof.
+intros.
+rewrite <- (div_mul q b) by order.
+apply div_le_mono; trivial. now rewrite mul_comm.
+Qed.
+
+Theorem div_le_lower_bound:
+  forall a b q, 0<b -> b*q <= a -> q <= a/b.
+Proof.
+intros.
+rewrite <- (div_mul q b) by order.
+apply div_le_mono; trivial. now rewrite mul_comm.
+Qed.
+
+(** A division respects opposite monotonicity for the divisor *)
+
+Lemma div_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p/r <= p/q.
+Proof. exact div_le_compat_l. Qed.
+
+(** * Relations between usual operations and mod and div *)
+
+Lemma mod_add : forall a b c, c~=0 ->
+ (a + b * c) mod c == a mod c.
+Proof.
+intros.
+symmetry.
+apply mod_unique with (a/c+b); trivial.
+now apply mod_bound_or.
+rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
+now rewrite mul_comm.
+Qed.
+
+Lemma div_add : forall a b c, c~=0 ->
+ (a + b * c) / c == a / c + b.
+Proof.
+intros.
+apply (mul_cancel_l _ _ c); try order.
+apply (add_cancel_r _ _ ((a+b*c) mod c)).
+rewrite <- div_mod, mod_add by order.
+rewrite mul_add_distr_l, add_shuffle0, <- div_mod by order.
+now rewrite mul_comm.
+Qed.
+
+Lemma div_add_l: forall a b c, b~=0 ->
+ (a * b + c) / b == a + c / b.
+Proof.
+ intros a b c. rewrite (add_comm _ c), (add_comm a).
+ now apply div_add.
+Qed.
+
+(** Cancellations. *)
+
+Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 ->
+ (a*c)/(b*c) == a/b.
+Proof.
+intros.
+symmetry.
+apply div_unique with ((a mod b)*c).
+(* ineqs *)
+destruct (lt_ge_cases 0 c).
+rewrite <-(mul_0_l c), <-2mul_lt_mono_pos_r, <-2mul_le_mono_pos_r by trivial.
+now apply mod_bound_or.
+rewrite <-(mul_0_l c), <-2mul_lt_mono_neg_r, <-2mul_le_mono_neg_r by order.
+destruct (mod_bound_or a b); tauto.
+(* equation *)
+rewrite (div_mod a b) at 1 by order.
+rewrite mul_add_distr_r.
+rewrite add_cancel_r.
+rewrite <- 2 mul_assoc. now rewrite (mul_comm c).
+Qed.
+
+Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 ->
+ (c*a)/(c*b) == a/b.
+Proof.
+intros. rewrite !(mul_comm c); now apply div_mul_cancel_r.
+Qed.
+
+Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 ->
+  (c*a) mod (c*b) == c * (a mod b).
+Proof.
+intros.
+rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))).
+rewrite <- div_mod.
+rewrite div_mul_cancel_l by trivial.
+rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
+apply div_mod; order.
+rewrite <- neq_mul_0; auto.
+Qed.
+
+Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 ->
+  (a*c) mod (b*c) == (a mod b) * c.
+Proof.
+ intros. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l.
+Qed.
+
+
+(** Operations modulo. *)
+
+Theorem mod_mod: forall a n, n~=0 ->
+ (a mod n) mod n == a mod n.
+Proof.
+intros. rewrite mod_small_iff by trivial.
+now apply mod_bound_or.
+Qed.
+
+Lemma mul_mod_idemp_l : forall a b n, n~=0 ->
+ ((a mod n)*b) mod n == (a*b) mod n.
+Proof.
+ intros a b n Hn. symmetry.
+ rewrite (div_mod a n) at 1 by order.
+ rewrite add_comm, (mul_comm n), (mul_comm _ b).
+ rewrite mul_add_distr_l, mul_assoc.
+ intros. rewrite mod_add by trivial.
+ now rewrite mul_comm.
+Qed.
+
+Lemma mul_mod_idemp_r : forall a b n, n~=0 ->
+ (a*(b mod n)) mod n == (a*b) mod n.
+Proof.
+ intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l.
+Qed.
+
+Theorem mul_mod: forall a b n, n~=0 ->
+ (a * b) mod n == ((a mod n) * (b mod n)) mod n.
+Proof.
+ intros. now rewrite mul_mod_idemp_l, mul_mod_idemp_r.
+Qed.
+
+Lemma add_mod_idemp_l : forall a b n, n~=0 ->
+ ((a mod n)+b) mod n == (a+b) mod n.
+Proof.
+ intros a b n Hn. symmetry.
+ rewrite (div_mod a n) at 1 by order.
+ rewrite <- add_assoc, add_comm, mul_comm.
+ intros. now rewrite mod_add.
+Qed.
+
+Lemma add_mod_idemp_r : forall a b n, n~=0 ->
+ (a+(b mod n)) mod n == (a+b) mod n.
+Proof.
+ intros. rewrite !(add_comm a). now apply add_mod_idemp_l.
+Qed.
+
+Theorem add_mod: forall a b n, n~=0 ->
+ (a+b) mod n == (a mod n + b mod n) mod n.
+Proof.
+ intros. now rewrite add_mod_idemp_l, add_mod_idemp_r.
+Qed.
+
+(** With the current convention, the following result isn't always
+    true for negative divisors. For instance
+    [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ]. *)
+
+Lemma div_div : forall a b c, 0<b -> 0<c ->
+ (a/b)/c == a/(b*c).
+Proof.
+ intros a b c Hb Hc.
+ apply div_unique with (b*((a/b) mod c) + a mod b).
+ (* begin 0<= ... <b*c \/ ... *)
+ left.
+ destruct (mod_pos_bound (a/b) c), (mod_pos_bound a b); trivial.
+ split.
+ apply add_nonneg_nonneg; trivial.
+ apply mul_nonneg_nonneg; order.
+ apply lt_le_trans with (b*((a/b) mod c) + b).
+ now rewrite <- add_lt_mono_l.
+ now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l.
+ (* end 0<= ... < b*c \/ ... *)
+ rewrite (div_mod a b) at 1 by order.
+ rewrite add_assoc, add_cancel_r.
+ rewrite <- mul_assoc, <- mul_add_distr_l, mul_cancel_l by order.
+ apply div_mod; order.
+Qed.
+
+(** A last inequality: *)
+
+Theorem div_mul_le:
+ forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b.
+Proof. exact div_mul_le. Qed.
+
+(** mod is related to divisibility *)
+
+Lemma mod_divides : forall a b, b~=0 ->
+ (a mod b == 0 <-> exists c, a == b*c).
+Proof.
+intros a b Hb. split.
+intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1.
+ rewrite Hab. now nzsimpl.
+intros (c,Hc).
+rewrite Hc, mul_comm.
+now apply mod_mul.
+Qed.
+
+End ZDivPropFunct.
+
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
new file mode 100644
index 00000000..3200ba2a
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -0,0 +1,532 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** * Euclidean Division for integers (Trunc convention)
+
+    We use here the convention known as Trunc, or Round-Toward-Zero,
+    where [a/b] is the integer with the largest absolute value to
+    be between zero and the exact fraction. It can be summarized by:
+
+    [a = bq+r /\ 0 <= |r| < |b| /\ Sign(r) = Sign(a)]
+
+    This is the convention of Ocaml and many other systems (C, ASM, ...).
+    This convention is named "T" in the following paper:
+
+    R. Boute, "The Euclidean definition of the functions div and mod",
+    ACM Transactions on Programming Languages and Systems,
+    Vol. 14, No.2, pp. 127-144, April 1992.
+
+    See files [ZDivFloor] and [ZDivEucl] for others conventions.
+*)
+
+Require Import ZAxioms ZProperties NZDiv.
+
+Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z).
+ Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
+ Axiom mod_opp_l : forall a b, b ~= 0 -> (-a) mod b == - (a mod b).
+ Axiom mod_opp_r : forall a b, b ~= 0 -> a mod (-b) == a mod b.
+End ZDivSpecific.
+
+Module Type ZDiv (Z:ZAxiomsSig)
+ := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
+
+Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation.
+
+Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
+
+(** We benefit from what already exists for NZ *)
+
+ Module Import NZDivP := NZDivPropFunct Z ZP Z.
+
+Ltac pos_or_neg a :=
+ let LT := fresh "LT" in
+ let LE := fresh "LE" in
+ destruct (le_gt_cases 0 a) as [LE|LT]; [|rewrite <- opp_pos_neg in LT].
+
+(** Another formulation of the main equation *)
+
+Lemma mod_eq :
+ forall a b, b~=0 -> a mod b == a - b*(a/b).
+Proof.
+intros.
+rewrite <- add_move_l.
+symmetry. now apply div_mod.
+Qed.
+
+(** A few sign rules (simple ones) *)
+
+Lemma mod_opp_opp : forall a b, b ~= 0 -> (-a) mod (-b) == - (a mod b).
+Proof. intros. now rewrite mod_opp_r, mod_opp_l. Qed.
+
+Lemma div_opp_l : forall a b, b ~= 0 -> (-a)/b == -(a/b).
+Proof.
+intros.
+rewrite <- (mul_cancel_l _ _ b) by trivial.
+rewrite <- (add_cancel_r _ _ ((-a) mod b)).
+now rewrite <- div_mod, mod_opp_l, mul_opp_r, <- opp_add_distr, <- div_mod.
+Qed.
+
+Lemma div_opp_r : forall a b, b ~= 0 -> a/(-b) == -(a/b).
+Proof.
+intros.
+assert (-b ~= 0) by (now rewrite eq_opp_l, opp_0).
+rewrite <- (mul_cancel_l _ _ (-b)) by trivial.
+rewrite <- (add_cancel_r _ _ (a mod (-b))).
+now rewrite <- div_mod, mod_opp_r, mul_opp_opp, <- div_mod.
+Qed.
+
+Lemma div_opp_opp : forall a b, b ~= 0 -> (-a)/(-b) == a/b.
+Proof. intros. now rewrite div_opp_r, div_opp_l, opp_involutive. Qed.
+
+(** The sign of [a mod b] is the one of [a] *)
+
+(* TODO: a proper sgn function and theory *)
+
+Lemma mod_sign : forall a b, b~=0 -> 0 <= (a mod b) * a.
+Proof.
+assert (Aux : forall a b, 0<b -> 0 <= (a mod b) * a).
+ intros. pos_or_neg a.
+ apply mul_nonneg_nonneg; trivial. now destruct (mod_bound a b).
+ rewrite <- mul_opp_opp, <- mod_opp_l by order.
+ apply mul_nonneg_nonneg; try order. destruct (mod_bound (-a) b); order.
+intros. pos_or_neg b. apply Aux; order.
+rewrite <- mod_opp_r by order. apply Aux; order.
+Qed.
+
+
+(** Uniqueness theorems *)
+
+Theorem div_mod_unique : forall b q1 q2 r1 r2 : t,
+  (0<=r1<b \/ b<r1<=0) -> (0<=r2<b \/ b<r2<=0) ->
+  b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2.
+Proof.
+intros b q1 q2 r1 r2 Hr1 Hr2 EQ.
+destruct Hr1; destruct Hr2; try (intuition; order).
+apply div_mod_unique with b; trivial.
+rewrite <- (opp_inj_wd r1 r2).
+apply div_mod_unique with (-b); trivial.
+rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.
+rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto.
+now rewrite 2 mul_opp_l, <- 2 opp_add_distr, opp_inj_wd.
+Qed.
+
+Theorem div_unique:
+ forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a/b.
+Proof. intros; now apply div_unique with r. Qed.
+
+Theorem mod_unique:
+ forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a mod b.
+Proof. intros; now apply mod_unique with q. Qed.
+
+(** A division by itself returns 1 *)
+
+Lemma div_same : forall a, a~=0 -> a/a == 1.
+Proof.
+intros. pos_or_neg a. apply div_same; order.
+rewrite <- div_opp_opp by trivial. now apply div_same.
+Qed.
+
+Lemma mod_same : forall a, a~=0 -> a mod a == 0.
+Proof.
+intros. rewrite mod_eq, div_same by trivial. nzsimpl. apply sub_diag.
+Qed.
+
+(** A division of a small number by a bigger one yields zero. *)
+
+Theorem div_small: forall a b, 0<=a<b -> a/b == 0.
+Proof. exact div_small. Qed.
+
+(** Same situation, in term of modulo: *)
+
+Theorem mod_small: forall a b, 0<=a<b -> a mod b == a.
+Proof. exact mod_small. Qed.
+
+(** * Basic values of divisions and modulo. *)
+
+Lemma div_0_l: forall a, a~=0 -> 0/a == 0.
+Proof.
+intros. pos_or_neg a. apply div_0_l; order.
+rewrite <- div_opp_opp, opp_0 by trivial. now apply div_0_l.
+Qed.
+
+Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0.
+Proof.
+intros; rewrite mod_eq, div_0_l; now nzsimpl.
+Qed.
+
+Lemma div_1_r: forall a, a/1 == a.
+Proof.
+intros. pos_or_neg a. now apply div_1_r.
+apply opp_inj. rewrite <- div_opp_l. apply div_1_r; order.
+intro EQ; symmetry in EQ; revert EQ; apply lt_neq, lt_0_1.
+Qed.
+
+Lemma mod_1_r: forall a, a mod 1 == 0.
+Proof.
+intros. rewrite mod_eq, div_1_r; nzsimpl; auto using sub_diag.
+intro EQ; symmetry in EQ; revert EQ; apply lt_neq; apply lt_0_1.
+Qed.
+
+Lemma div_1_l: forall a, 1<a -> 1/a == 0.
+Proof. exact div_1_l. Qed.
+
+Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
+Proof. exact mod_1_l. Qed.
+
+Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a.
+Proof.
+intros. pos_or_neg a; pos_or_neg b. apply div_mul; order.
+rewrite <- div_opp_opp, <- mul_opp_r by order. apply div_mul; order.
+rewrite <- opp_inj_wd, <- div_opp_l, <- mul_opp_l by order. apply div_mul; order.
+rewrite <- opp_inj_wd, <- div_opp_r, <- mul_opp_opp by order. apply div_mul; order.
+Qed.
+
+Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0.
+Proof.
+intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
+Qed.
+
+(** * Order results about mod and div *)
+
+(** A modulo cannot grow beyond its starting point. *)
+
+Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a.
+Proof. exact mod_le. Qed.
+
+Theorem div_pos : forall a b, 0<=a -> 0<b -> 0<= a/b.
+Proof. exact div_pos. Qed.
+
+Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.
+Proof. exact div_str_pos. Qed.
+
+Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> abs a < abs b).
+Proof.
+intros. pos_or_neg a; pos_or_neg b.
+rewrite div_small_iff; try order. rewrite 2 abs_eq; intuition; order.
+rewrite <- opp_inj_wd, opp_0, <- div_opp_r, div_small_iff by order.
+ rewrite (abs_eq a), (abs_neq' b); intuition; order.
+rewrite <- opp_inj_wd, opp_0, <- div_opp_l, div_small_iff by order.
+ rewrite (abs_neq' a), (abs_eq b); intuition; order.
+rewrite <- div_opp_opp, div_small_iff by order.
+ rewrite (abs_neq' a), (abs_neq' b); intuition; order.
+Qed.
+
+Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> abs a < abs b).
+Proof.
+intros. rewrite mod_eq, <- div_small_iff by order.
+rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l.
+rewrite eq_sym_iff, eq_mul_0. tauto.
+Qed.
+
+(** As soon as the divisor is strictly greater than 1,
+    the division is strictly decreasing. *)
+
+Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a.
+Proof. exact div_lt. Qed.
+
+(** [le] is compatible with a positive division. *)
+
+Lemma div_le_mono : forall a b c, 0<c -> a<=b -> a/c <= b/c.
+Proof.
+intros. pos_or_neg a. apply div_le_mono; auto.
+pos_or_neg b. apply le_trans with 0.
+ rewrite <- opp_nonneg_nonpos, <- div_opp_l by order.
+ apply div_pos; order.
+ apply div_pos; order.
+rewrite opp_le_mono in *. rewrite <- 2 div_opp_l by order.
+ apply div_le_mono; intuition; order.
+Qed.
+
+(** With this choice of division,
+    rounding of div is always done toward zero: *)
+
+Lemma mul_div_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a/b) <= a.
+Proof.
+intros. pos_or_neg b.
+split.
+apply mul_nonneg_nonneg; [|apply div_pos]; order.
+apply mul_div_le; order.
+rewrite <- mul_opp_opp, <- div_opp_r by order.
+split.
+apply mul_nonneg_nonneg; [|apply div_pos]; order.
+apply mul_div_le; order.
+Qed.
+
+Lemma mul_div_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a/b) <= 0.
+Proof.
+intros.
+rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-div_opp_l by order.
+rewrite <- opp_nonneg_nonpos in *.
+destruct (mul_div_le (-a) b); tauto.
+Qed.
+
+(** For positive numbers, considering [S (a/b)] leads to an upper bound for [a] *)
+
+Lemma mul_succ_div_gt: forall a b, 0<=a -> 0<b -> a < b*(S (a/b)).
+Proof. exact mul_succ_div_gt. Qed.
+
+(** Similar results with negative numbers *)
+
+Lemma mul_pred_div_lt: forall a b, a<=0 -> 0<b -> b*(P (a/b)) < a.
+Proof.
+intros.
+rewrite opp_lt_mono, <- mul_opp_r, opp_pred, <- div_opp_l by order.
+rewrite <- opp_nonneg_nonpos in *.
+now apply mul_succ_div_gt.
+Qed.
+
+Lemma mul_pred_div_gt: forall a b, 0<=a -> b<0 -> a < b*(P (a/b)).
+Proof.
+intros.
+rewrite <- mul_opp_opp, opp_pred, <- div_opp_r by order.
+rewrite <- opp_pos_neg in *.
+now apply mul_succ_div_gt.
+Qed.
+
+Lemma mul_succ_div_lt: forall a b, a<=0 -> b<0 -> b*(S (a/b)) < a.
+Proof.
+intros.
+rewrite opp_lt_mono, <- mul_opp_l, <- div_opp_opp by order.
+rewrite <- opp_nonneg_nonpos, <- opp_pos_neg in *.
+now apply mul_succ_div_gt.
+Qed.
+
+(** Inequality [mul_div_le] is exact iff the modulo is zero. *)
+
+Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).
+Proof.
+intros. rewrite mod_eq by order. rewrite sub_move_r; nzsimpl; tauto.
+Qed.
+
+(** Some additionnal inequalities about div. *)
+
+Theorem div_lt_upper_bound:
+  forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q.
+Proof. exact div_lt_upper_bound. Qed.
+
+Theorem div_le_upper_bound:
+  forall a b q, 0<b -> a <= b*q -> a/b <= q.
+Proof.
+intros.
+rewrite <- (div_mul q b) by order.
+apply div_le_mono; trivial. now rewrite mul_comm.
+Qed.
+
+Theorem div_le_lower_bound:
+  forall a b q, 0<b -> b*q <= a -> q <= a/b.
+Proof.
+intros.
+rewrite <- (div_mul q b) by order.
+apply div_le_mono; trivial. now rewrite mul_comm.
+Qed.
+
+(** A division respects opposite monotonicity for the divisor *)
+
+Lemma div_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p/r <= p/q.
+Proof. exact div_le_compat_l. Qed.
+
+(** * Relations between usual operations and mod and div *)
+
+(** Unlike with other division conventions, some results here aren't
+    always valid, and need to be restricted. For instance
+    [(a+b*c) mod c <> a mod c] for [a=9,b=-5,c=2] *)
+
+Lemma mod_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a ->
+ (a + b * c) mod c == a mod c.
+Proof.
+assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) mod c == a mod c).
+ intros. pos_or_neg c. apply mod_add; order.
+ rewrite <- (mod_opp_r a), <- (mod_opp_r (a+b*c)) by order.
+ rewrite <- mul_opp_opp in *.
+ apply mod_add; order.
+intros a b c Hc Habc.
+destruct (le_0_mul _ _ Habc) as [(Habc',Ha)|(Habc',Ha)]. auto.
+apply opp_inj. revert Ha Habc'.
+rewrite <- 2 opp_nonneg_nonpos.
+rewrite <- 2 mod_opp_l, opp_add_distr, <- mul_opp_l by order. auto.
+Qed.
+
+Lemma div_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a ->
+ (a + b * c) / c == a / c + b.
+Proof.
+intros.
+rewrite <- (mul_cancel_l _ _ c) by trivial.
+rewrite <- (add_cancel_r _ _ ((a+b*c) mod c)).
+rewrite <- div_mod, mod_add by trivial.
+now rewrite mul_add_distr_l, add_shuffle0, <-div_mod, mul_comm.
+Qed.
+
+Lemma div_add_l: forall a b c, b~=0 -> 0 <= (a*b+c)*c ->
+ (a * b + c) / b == a + c / b.
+Proof.
+ intros a b c. rewrite add_comm, (add_comm a). now apply div_add.
+Qed.
+
+(** Cancellations. *)
+
+Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 ->
+ (a*c)/(b*c) == a/b.
+Proof.
+assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)/(b*c) == a/b).
+ intros. pos_or_neg c. apply div_mul_cancel_r; order.
+ rewrite <- div_opp_opp, <- 2 mul_opp_r. apply div_mul_cancel_r; order.
+ rewrite <- neq_mul_0; intuition order.
+assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)/(b*c) == a/b).
+ intros. pos_or_neg b. apply Aux1; order.
+ apply opp_inj. rewrite <- 2 div_opp_r, <- mul_opp_l; try order. apply Aux1; order.
+ rewrite <- neq_mul_0; intuition order.
+intros. pos_or_neg a. apply Aux2; order.
+apply opp_inj. rewrite <- 2 div_opp_l, <- mul_opp_l; try order. apply Aux2; order.
+rewrite <- neq_mul_0; intuition order.
+Qed.
+
+Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 ->
+ (c*a)/(c*b) == a/b.
+Proof.
+intros. rewrite !(mul_comm c); now apply div_mul_cancel_r.
+Qed.
+
+Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 ->
+  (a*c) mod (b*c) == (a mod b) * c.
+Proof.
+intros.
+assert (b*c ~= 0) by (rewrite <- neq_mul_0; tauto).
+rewrite ! mod_eq by trivial.
+rewrite div_mul_cancel_r by order.
+now rewrite mul_sub_distr_r, <- !mul_assoc, (mul_comm (a/b) c).
+Qed.
+
+Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 ->
+  (c*a) mod (c*b) == c * (a mod b).
+Proof.
+intros; rewrite !(mul_comm c); now apply mul_mod_distr_r.
+Qed.
+
+(** Operations modulo. *)
+
+Theorem mod_mod: forall a n, n~=0 ->
+ (a mod n) mod n == a mod n.
+Proof.
+intros. pos_or_neg a; pos_or_neg n. apply mod_mod; order.
+rewrite <- ! (mod_opp_r _ n) by trivial. apply mod_mod; order.
+apply opp_inj. rewrite <- !mod_opp_l by order. apply mod_mod; order.
+apply opp_inj. rewrite <- !mod_opp_opp by order. apply mod_mod; order.
+Qed.
+
+Lemma mul_mod_idemp_l : forall a b n, n~=0 ->
+ ((a mod n)*b) mod n == (a*b) mod n.
+Proof.
+assert (Aux1 : forall a b n, 0<=a -> 0<=b -> n~=0 ->
+         ((a mod n)*b) mod n == (a*b) mod n).
+ intros. pos_or_neg n. apply mul_mod_idemp_l; order.
+ rewrite <- ! (mod_opp_r _ n) by order. apply mul_mod_idemp_l; order.
+assert (Aux2 : forall a b n, 0<=a -> n~=0 ->
+         ((a mod n)*b) mod n == (a*b) mod n).
+ intros. pos_or_neg b. now apply Aux1.
+ apply opp_inj. rewrite <-2 mod_opp_l, <-2 mul_opp_r by order.
+  apply Aux1; order.
+intros a b n Hn. pos_or_neg a. now apply Aux2.
+apply opp_inj. rewrite <-2 mod_opp_l, <-2 mul_opp_l, <-mod_opp_l by order.
+apply Aux2; order.
+Qed.
+
+Lemma mul_mod_idemp_r : forall a b n, n~=0 ->
+ (a*(b mod n)) mod n == (a*b) mod n.
+Proof.
+intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l.
+Qed.
+
+Theorem mul_mod: forall a b n, n~=0 ->
+ (a * b) mod n == ((a mod n) * (b mod n)) mod n.
+Proof.
+intros. now rewrite mul_mod_idemp_l, mul_mod_idemp_r.
+Qed.
+
+(** addition and modulo
+
+  Generally speaking, unlike with other conventions, we don't have
+       [(a+b) mod n = (a mod n + b mod n) mod n]
+  for any a and b.
+  For instance, take (8 + (-10)) mod 3 = -2 whereas
+  (8 mod 3 + (-10 mod 3)) mod 3 = 1.
+*)
+
+Lemma add_mod_idemp_l : forall a b n, n~=0 -> 0 <= a*b ->
+ ((a mod n)+b) mod n == (a+b) mod n.
+Proof.
+assert (Aux : forall a b n, 0<=a -> 0<=b -> n~=0 ->
+          ((a mod n)+b) mod n == (a+b) mod n).
+ intros. pos_or_neg n. apply add_mod_idemp_l; order.
+ rewrite <- ! (mod_opp_r _ n) by order. apply add_mod_idemp_l; order.
+intros a b n Hn Hab. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)].
+now apply Aux.
+apply opp_inj. rewrite <-2 mod_opp_l, 2 opp_add_distr, <-mod_opp_l by order.
+rewrite <- opp_nonneg_nonpos in *.
+now apply Aux.
+Qed.
+
+Lemma add_mod_idemp_r : forall a b n, n~=0 -> 0 <= a*b ->
+ (a+(b mod n)) mod n == (a+b) mod n.
+Proof.
+intros. rewrite !(add_comm a). apply add_mod_idemp_l; trivial.
+now rewrite mul_comm.
+Qed.
+
+Theorem add_mod: forall a b n, n~=0 -> 0 <= a*b ->
+ (a+b) mod n == (a mod n + b mod n) mod n.
+Proof.
+intros a b n Hn Hab. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial.
+reflexivity.
+destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)];
+ destruct (le_0_mul _ _ (mod_sign b n Hn)) as [(Hb',Hm)|(Hb',Hm)];
+ auto using mul_nonneg_nonneg, mul_nonpos_nonpos.
+ setoid_replace b with 0 by order. rewrite mod_0_l by order. nzsimpl; order.
+ setoid_replace b with 0 by order. rewrite mod_0_l by order. nzsimpl; order.
+Qed.
+
+
+(** Conversely, the following result needs less restrictions here. *)
+
+Lemma div_div : forall a b c, b~=0 -> c~=0 ->
+ (a/b)/c == a/(b*c).
+Proof.
+assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a/b)/c == a/(b*c)).
+ intros. pos_or_neg c. apply div_div; order.
+ apply opp_inj. rewrite <- 2 div_opp_r, <- mul_opp_r; trivial.
+ apply div_div; order.
+ rewrite <- neq_mul_0; intuition order.
+assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a/b)/c == a/(b*c)).
+ intros. pos_or_neg b. apply Aux1; order.
+ apply opp_inj. rewrite <- div_opp_l, <- 2 div_opp_r, <- mul_opp_l; trivial.
+ apply Aux1; trivial.
+ rewrite <- neq_mul_0; intuition order.
+intros. pos_or_neg a. apply Aux2; order.
+apply opp_inj. rewrite <- 3 div_opp_l; try order. apply Aux2; order.
+rewrite <- neq_mul_0. tauto.
+Qed.
+
+(** A last inequality: *)
+
+Theorem div_mul_le:
+ forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b.
+Proof. exact div_mul_le. Qed.
+
+(** mod is related to divisibility *)
+
+Lemma mod_divides : forall a b, b~=0 ->
+ (a mod b == 0 <-> exists c, a == b*c).
+Proof.
+ intros a b Hb. split.
+ intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1.
+  rewrite Hab; now nzsimpl.
+ intros (c,Hc). rewrite Hc, mul_comm. now apply mod_mul.
+Qed.
+
+End ZDivPropFunct.
+
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
deleted file mode 100644
index 9a17e151..00000000
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ /dev/null
@@ -1,69 +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: ZDomain.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
-
-Require Export NumPrelude.
-
-Module Type ZDomainSignature.
-
-Parameter Inline Z : Set.
-Parameter Inline Zeq : Z -> Z -> Prop.
-Parameter Inline e : Z -> Z -> bool.
-
-Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y.
-Axiom eq_equiv : equiv Z Zeq.
-
-Add Relation Z Zeq
- reflexivity proved by (proj1 eq_equiv)
- symmetry proved by (proj2 (proj2 eq_equiv))
- transitivity proved by (proj1 (proj2 eq_equiv))
-as eq_rel.
-
-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.
-
-Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
-Proof.
-intros x x' Exx' y y' Eyy'.
-case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
-assert (x == y); [apply <- eq_equiv_e; now rewrite H2 |
-assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
-rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]].
-assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 |
-assert (x == y); [rewrite Exx'; now rewrite Eyy' |
-rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
-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 (proj1 (proj2 eq_equiv)).
-
-End ZDomainProperties.
-
-
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 2a88a535..849bf6b4 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -8,424 +8,126 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZLt.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id$ i*)
 
 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.
 
-(* 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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, predicate_wd Zeq 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 c48d1b4c..84d840ad 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -8,106 +8,63 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export ZAdd.
 
-Module ZMulPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZAddPropMod := ZAddPropFunct ZAxiomsMod.
-Open Local Scope IntScope.
+Module ZMulPropFunct (Import Z : ZAxiomsSig').
+Include ZAddPropFunct Z.
 
-Theorem Zmul_wd :
-  forall n1 n2 : Z, n1 == n2 -> forall m1 m2 : Z, m1 == m2 -> n1 * m1 == n2 * m2.
-Proof NZmul_wd.
+(** 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_0_l : forall n : Z, 0 * n == 0.
-Proof NZmul_0_l.
+(** Theorems that are either not valid on N or have different proofs
+    on N and Z *)
 
-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.
+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 c7996ffd..99be58eb 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -8,335 +8,225 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: ZMulOrder.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
+(*i $Id$ i*)
 
 Require Export ZAddOrder.
 
-Module ZMulOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
-Module Export ZAddOrderPropMod := ZAddOrderPropFunct ZAxiomsMod.
-Open Local Scope IntScope.
+Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig').
+Include ZAddOrderPropFunct Z.
 
-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.
+Local Notation "- 1" := (-(1)).
 
-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].
-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.
-Proof.
-intros n m H1 H2.
-rewrite <- (Zmul_0_l m). now apply Zmul_le_mono_nonneg_r.
+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_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.
+Notation mul_pos := lt_0_mul (only parsing).
 
-Theorem Zeq_mul_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
-Proof NZeq_mul_0_l.
-
-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.
-elimtype False; now apply (Zlt_asymm (n * m) 0).
-assert (H3 : n * m > 0) by now apply Zmul_pos_pos.
-elimtype False; 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 00000000..dc46edda
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*  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 ZSgnAbs.
+
+(** This functor summarizes all known facts about Z.
+    For the moment it is only an alias to [ZMulOrderPropFunct], which
+    subsumes all others, plus properties of [sgn] and [abs].
+*)
+
+Module Type ZPropSig (Z:ZAxiomsExtSig) :=
+ ZMulOrderPropFunct Z <+ ZSgnAbsPropSig Z.
+
+Module ZPropFunct (Z:ZAxiomsExtSig) <: ZPropSig Z.
+ Include ZPropSig Z.
+End ZPropFunct.
+
diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
new file mode 100644
index 00000000..8b191613
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
@@ -0,0 +1,348 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Export ZMulOrder.
+
+(** An axiomatization of [abs]. *)
+
+Module Type HasAbs(Import Z : ZAxiomsSig').
+ Parameter Inline abs : t -> t.
+ Axiom abs_eq : forall n, 0<=n -> abs n == n.
+ Axiom abs_neq : forall n, n<=0 -> abs n == -n.
+End HasAbs.
+
+(** Since we already have [max], we could have defined [abs]. *)
+
+Module GenericAbs (Import Z : ZAxiomsSig')
+                  (Import ZP : ZMulOrderPropFunct Z) <: HasAbs Z.
+ Definition abs n := max n (-n).
+ Lemma abs_eq : forall n, 0<=n -> abs n == n.
+ Proof.
+  intros. unfold abs. apply max_l.
+  apply le_trans with 0; auto.
+  rewrite opp_nonpos_nonneg; auto.
+ Qed.
+ Lemma abs_neq : forall n, n<=0 -> abs n == -n.
+ Proof.
+  intros. unfold abs. apply max_r.
+  apply le_trans with 0; auto.
+  rewrite opp_nonneg_nonpos; auto.
+ Qed.
+End GenericAbs.
+
+(** An Axiomatization of [sgn]. *)
+
+Module Type HasSgn (Import Z : ZAxiomsSig').
+ Parameter Inline sgn : t -> t.
+ Axiom sgn_null : forall n, n==0 -> sgn n == 0.
+ Axiom sgn_pos : forall n, 0<n -> sgn n == 1.
+ Axiom sgn_neg : forall n, n<0 -> sgn n == -(1).
+End HasSgn.
+
+(** We can deduce a [sgn] function from a [compare] function *)
+
+Module Type ZDecAxiomsSig := ZAxiomsSig <+ HasCompare.
+Module Type ZDecAxiomsSig' := ZAxiomsSig' <+ HasCompare.
+
+Module Type GenericSgn (Import Z : ZDecAxiomsSig')
+                       (Import ZP : ZMulOrderPropFunct Z) <: HasSgn Z.
+ Definition sgn n :=
+  match compare 0 n with Eq => 0 | Lt => 1 | Gt => -(1) end.
+ Lemma sgn_null : forall n, n==0 -> sgn n == 0.
+ Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
+ Lemma sgn_pos : forall n, 0<n -> sgn n == 1.
+ Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
+ Lemma sgn_neg : forall n, n<0 -> sgn n == -(1).
+ Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
+End GenericSgn.
+
+Module Type ZAxiomsExtSig := ZAxiomsSig <+ HasAbs <+ HasSgn.
+Module Type ZAxiomsExtSig' := ZAxiomsSig' <+ HasAbs <+ HasSgn.
+
+Module Type ZSgnAbsPropSig (Import Z : ZAxiomsExtSig')
+                           (Import ZP : ZMulOrderPropFunct Z).
+
+Ltac destruct_max n :=
+ destruct (le_ge_cases 0 n);
+  [rewrite (abs_eq n) by auto | rewrite (abs_neq n) by auto].
+
+Instance abs_wd : Proper (eq==>eq) abs.
+Proof.
+ intros x y EQ. destruct_max x.
+ rewrite abs_eq; trivial. now rewrite <- EQ.
+ rewrite abs_neq; try order. now rewrite opp_inj_wd.
+Qed.
+
+Lemma abs_max : forall n, abs n == max n (-n).
+Proof.
+ intros n. destruct_max n.
+ rewrite max_l; auto with relations.
+ apply le_trans with 0; auto.
+ rewrite opp_nonpos_nonneg; auto.
+ rewrite max_r; auto with relations.
+ apply le_trans with 0; auto.
+ rewrite opp_nonneg_nonpos; auto.
+Qed.
+
+Lemma abs_neq' : forall n, 0<=-n -> abs n == -n.
+Proof.
+ intros. apply abs_neq. now rewrite <- opp_nonneg_nonpos.
+Qed.
+
+Lemma abs_nonneg : forall n, 0 <= abs n.
+Proof.
+ intros n. destruct_max n; auto.
+ now rewrite opp_nonneg_nonpos.
+Qed.
+
+Lemma abs_eq_iff : forall n, abs n == n <-> 0<=n.
+Proof.
+ split; try apply abs_eq. intros EQ.
+ rewrite <- EQ. apply abs_nonneg.
+Qed.
+
+Lemma abs_neq_iff : forall n, abs n == -n <-> n<=0.
+Proof.
+ split; try apply abs_neq. intros EQ.
+ rewrite <- opp_nonneg_nonpos, <- EQ. apply abs_nonneg.
+Qed.
+
+Lemma abs_opp : forall n, abs (-n) == abs n.
+Proof.
+ intros. destruct_max n.
+ rewrite (abs_neq (-n)), opp_involutive. reflexivity.
+ now rewrite opp_nonpos_nonneg.
+ rewrite (abs_eq (-n)). reflexivity.
+ now rewrite opp_nonneg_nonpos.
+Qed.
+
+Lemma abs_0 : abs 0 == 0.
+Proof.
+ apply abs_eq. apply le_refl.
+Qed.
+
+Lemma abs_0_iff : forall n, abs n == 0 <-> n==0.
+Proof.
+ split. destruct_max n; auto.
+ now rewrite eq_opp_l, opp_0.
+ intros EQ; rewrite EQ. rewrite abs_eq; auto using eq_refl, le_refl.
+Qed.
+
+Lemma abs_pos : forall n, 0 < abs n <-> n~=0.
+Proof.
+ intros. rewrite <- abs_0_iff. split; [intros LT| intros NEQ].
+ intro EQ. rewrite EQ in LT. now elim (lt_irrefl 0).
+ assert (LE : 0 <= abs n) by apply abs_nonneg.
+ rewrite lt_eq_cases in LE; destruct LE; auto.
+ elim NEQ; auto with relations.
+Qed.
+
+Lemma abs_eq_or_opp : forall n, abs n == n \/ abs n == -n.
+Proof.
+ intros. destruct_max n; auto with relations.
+Qed.
+
+Lemma abs_or_opp_abs : forall n, n == abs n \/ n == - abs n.
+Proof.
+ intros. destruct_max n; rewrite ? opp_involutive; auto with relations.
+Qed.
+
+Lemma abs_involutive : forall n, abs (abs n) == abs n.
+Proof.
+ intros. apply abs_eq. apply abs_nonneg.
+Qed.
+
+Lemma abs_spec : forall n,
+  (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n).
+Proof.
+ intros. destruct (le_gt_cases 0 n).
+ left; split; auto. now apply abs_eq.
+ right; split; auto. apply abs_neq. now apply lt_le_incl.
+Qed.
+
+Lemma abs_case_strong :
+  forall (P:t->Prop) n, Proper (eq==>iff) P ->
+    (0<=n -> P n) -> (n<=0 -> P (-n)) -> P (abs n).
+Proof.
+ intros. destruct_max n; auto.
+Qed.
+
+Lemma abs_case : forall (P:t->Prop) n, Proper (eq==>iff) P ->
+ P n -> P (-n) -> P (abs n).
+Proof. intros. now apply abs_case_strong. Qed.
+
+Lemma abs_eq_cases : forall n m, abs n == abs m -> n == m \/ n == - m.
+Proof.
+ intros n m EQ. destruct (abs_or_opp_abs n) as [EQn|EQn].
+ rewrite EQn, EQ. apply abs_eq_or_opp.
+ rewrite EQn, EQ, opp_inj_wd, eq_opp_l, or_comm. apply abs_eq_or_opp.
+Qed.
+
+(** Triangular inequality *)
+
+Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m.
+Proof.
+ intros. destruct_max n; destruct_max m.
+ rewrite abs_eq. apply le_refl. now apply add_nonneg_nonneg.
+ destruct_max (n+m); try rewrite opp_add_distr;
+  apply add_le_mono_l || apply add_le_mono_r.
+ apply le_trans with 0; auto. now rewrite opp_nonneg_nonpos.
+ apply le_trans with 0; auto. now rewrite opp_nonpos_nonneg.
+ destruct_max (n+m); try rewrite opp_add_distr;
+  apply add_le_mono_l || apply add_le_mono_r.
+ apply le_trans with 0; auto. now rewrite opp_nonneg_nonpos.
+ apply le_trans with 0; auto. now rewrite opp_nonpos_nonneg.
+ rewrite abs_neq, opp_add_distr. apply le_refl.
+ now apply add_nonpos_nonpos.
+Qed.
+
+Lemma abs_sub_triangle : forall n m, abs n - abs m <= abs (n-m).
+Proof.
+ intros.
+ rewrite le_sub_le_add_l, add_comm.
+ rewrite <- (sub_simpl_r n m) at 1.
+ apply abs_triangle.
+Qed.
+
+(** Absolute value and multiplication *)
+
+Lemma abs_mul : forall n m, abs (n * m) == abs n * abs m.
+Proof.
+ assert (H : forall n m, 0<=n -> abs (n*m) == n * abs m).
+  intros. destruct_max m.
+  rewrite abs_eq. apply eq_refl. now apply mul_nonneg_nonneg.
+  rewrite abs_neq, mul_opp_r. reflexivity. now apply mul_nonneg_nonpos .
+ intros. destruct_max n. now apply H.
+ rewrite <- mul_opp_opp, H, abs_opp. reflexivity.
+ now apply opp_nonneg_nonpos.
+Qed.
+
+Lemma abs_square : forall n, abs n * abs n == n * n.
+Proof.
+ intros. rewrite <- abs_mul. apply abs_eq. apply le_0_square.
+Qed.
+
+(** Some results about the sign function. *)
+
+Ltac destruct_sgn n :=
+ let LT := fresh "LT" in
+ let EQ := fresh "EQ" in
+ let GT := fresh "GT" in
+ destruct (lt_trichotomy 0 n) as [LT|[EQ|GT]];
+ [rewrite (sgn_pos n) by auto|
+  rewrite (sgn_null n) by auto with relations|
+  rewrite (sgn_neg n) by auto].
+
+Instance sgn_wd : Proper (eq==>eq) sgn.
+Proof.
+ intros x y Hxy. destruct_sgn x.
+ rewrite sgn_pos; auto with relations. rewrite <- Hxy; auto.
+ rewrite sgn_null; auto with relations. rewrite <- Hxy; auto with relations.
+ rewrite sgn_neg; auto with relations. rewrite <- Hxy; auto.
+Qed.
+
+Lemma sgn_spec : forall n,
+  0 < n /\ sgn n == 1 \/
+  0 == n /\ sgn n == 0 \/
+  0 > n /\ sgn n == -(1).
+Proof.
+ intros n.
+ destruct_sgn n; [left|right;left|right;right]; auto with relations.
+Qed.
+
+Lemma sgn_0 : sgn 0 == 0.
+Proof.
+ now apply sgn_null.
+Qed.
+
+Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n.
+Proof.
+ split; try apply sgn_pos. destruct_sgn n; auto.
+ intros. elim (lt_neq 0 1); auto. apply lt_0_1.
+ intros. elim (lt_neq (-(1)) 1); auto.
+ apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1.
+Qed.
+
+Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0.
+Proof.
+ split; try apply sgn_null. destruct_sgn n; auto with relations.
+ intros. elim (lt_neq 0 1); auto with relations. apply lt_0_1.
+ intros. elim (lt_neq (-(1)) 0); auto.
+ rewrite opp_neg_pos. apply lt_0_1.
+Qed.
+
+Lemma sgn_neg_iff : forall n, sgn n == -(1) <-> n<0.
+Proof.
+ split; try apply sgn_neg. destruct_sgn n; auto with relations.
+ intros. elim (lt_neq (-(1)) 1); auto with relations.
+ apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1.
+ intros. elim (lt_neq (-(1)) 0); auto with relations.
+ rewrite opp_neg_pos. apply lt_0_1.
+Qed.
+
+Lemma sgn_opp : forall n, sgn (-n) == - sgn n.
+Proof.
+ intros. destruct_sgn n.
+ apply sgn_neg. now rewrite opp_neg_pos.
+ setoid_replace n with 0 by auto with relations.
+  rewrite opp_0. apply sgn_0.
+ rewrite opp_involutive. apply sgn_pos. now rewrite opp_pos_neg.
+Qed.
+
+Lemma sgn_nonneg : forall n, 0 <= sgn n <-> 0 <= n.
+Proof.
+ split.
+ destruct_sgn n; intros.
+ now apply lt_le_incl.
+ order.
+ elim (lt_irrefl 0). apply lt_le_trans with 1; auto using lt_0_1.
+  now rewrite <- opp_nonneg_nonpos.
+ rewrite lt_eq_cases; destruct 1.
+ rewrite sgn_pos by auto. apply lt_le_incl, lt_0_1.
+ rewrite sgn_null by auto with relations. apply le_refl.
+Qed.
+
+Lemma sgn_nonpos : forall n, sgn n <= 0 <-> n <= 0.
+Proof.
+ intros. rewrite <- 2 opp_nonneg_nonpos, <- sgn_opp. apply sgn_nonneg.
+Qed.
+
+Lemma sgn_mul : forall n m, sgn (n*m) == sgn n * sgn m.
+Proof.
+ intros. destruct_sgn n; nzsimpl.
+ destruct_sgn m.
+  apply sgn_pos. now apply mul_pos_pos.
+  apply sgn_null. rewrite eq_mul_0; auto with relations.
+  apply sgn_neg. now apply mul_pos_neg.
+ apply sgn_null. rewrite eq_mul_0; auto with relations.
+ destruct_sgn m; try rewrite mul_opp_opp; nzsimpl.
+  apply sgn_neg. now apply mul_neg_pos.
+  apply sgn_null. rewrite eq_mul_0; auto with relations.
+  apply sgn_pos. now apply mul_neg_neg.
+Qed.
+
+Lemma sgn_abs : forall n, n * sgn n == abs n.
+Proof.
+ intros. symmetry.
+ destruct_sgn n; try rewrite mul_opp_r; nzsimpl.
+ apply abs_eq. now apply lt_le_incl.
+ rewrite abs_0_iff; auto with relations.
+ apply abs_neq. now apply lt_le_incl.
+Qed.
+
+Lemma abs_sgn : forall n, abs n * sgn n == n.
+Proof.
+ intros.
+ destruct_sgn n; try rewrite mul_opp_r; nzsimpl; auto.
+ apply abs_eq. now apply lt_le_incl.
+ rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl.
+Qed.
+
+End ZSgnAbsPropSig.
+
+