Integer division: quot and rem (trunc convention) in addition to div and mod

(floor convention).

We follow Haskell naming convention: quot and rem are for
Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf.
the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom
(a.k.a Floor, what Coq does historically in Zdiv). We use unicode ÷
for quot, and infix rem for rem (which is actually remainder in
full). This way, both conventions can be used at the same time.

Definitions (and proofs of specifications) for div mod quot rem are
migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With
this new organisation, no need for functor application in Zdiv and
Zquot.

On the abstract side, ZAxiomsSig now provides div mod quot rem.
Zproperties now contains properties of them. In NZDiv, we stop
splitting specifications in Common vs. Specific parts. Instead,
the NZ specification is be extended later, even if this leads to
a useless mod_bound_pos, subsumed by more precise axioms.

A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff).

A few proofs in Nnat, Znat, Zabs are reworked (no more dependency
to Zmin, Zmax).

A lcm (least common multiple) is derived abstractly from gcd and
division (and hence available for nat N BigN Z BigZ :-).
In these new files NLcm and ZLcm, we also provide some combined
properties of div mod quot rem gcd.

We also provide a new file Zeuclid implementing a third division
convention, where the remainder is always positive. This file
instanciate the abstract one ZDivEucl. Operation names are
ZEuclid.div and ZEuclid.modulo.

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

12 files changed, 991 insertions, 367 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 754c0b3d1..89fa8e170 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Export NZAxioms.
-Require Import NZPow NZSqrt NZLog NZGcd.
+Require Import NZPow NZSqrt NZLog NZGcd NZDiv.
 
 (** We obtain integers by postulating that successor of predecessor
     is identity. *)
@@ -70,16 +70,56 @@ Module Type Parity (Import Z : ZAxiomsMiniSig').
  Axiom odd_spec : forall n, odd n = true <-> Odd n.
 End Parity.
 
+(** Divisions *)
+
+(** First, the usual Coq convention of Truncated-Toward-Bottom
+    (a.k.a Floor). We simply extend the NZ signature. *)
+
+Module Type ZDivSpecific (Import A:ZAxiomsMiniSig')(Import B : DivMod' A).
+ 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:ZAxiomsMiniSig) := NZDiv.NZDiv Z <+ ZDivSpecific Z.
+Module Type ZDiv' (Z:ZAxiomsMiniSig) := NZDiv.NZDiv' Z <+ ZDivSpecific Z.
+
+(** Then, the Truncated-Toward-Zero convention.
+    For not colliding with Floor operations, we use different names
+*)
+
+Module Type QuotRem (Import A : Typ).
+ Parameters Inline quot remainder : t -> t -> t.
+End QuotRem.
+
+Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A).
+ Infix "÷" := quot (at level 40, left associativity).
+ Infix "rem" := remainder (at level 40, no associativity).
+End QuotRemNotation.
+
+Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A.
+
+Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A).
+ Declare Instance quot_wd : Proper (eq==>eq==>eq) quot.
+ Declare Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+ Axiom quot_rem : forall a b, b ~= 0 -> a == b*(a÷b) + (a rem b).
+ Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
+ Axiom rem_opp_l : forall a b, b ~= 0 -> (-a) rem b == - (a rem b).
+ Axiom rem_opp_r : forall a b, b ~= 0 -> a rem (-b) == a rem b.
+End QuotRemSpec.
+
+Module Type ZQuot (Z:ZAxiomsMiniSig) := QuotRem Z <+ QuotRemSpec Z.
+Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.
+
 (** For pow sqrt log2 gcd, the NZ axiomatizations are enough. *)
 
 (** Let's group everything *)
 
 Module Type ZAxiomsSig :=
   ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd.
+   <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
+   <+ ZDiv <+ ZQuot.
+
 Module Type ZAxiomsSig' :=
   ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'.
-
-
-(** Division is left apart, since many different flavours are available *)
+   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
+   <+ ZDiv' <+ ZQuot'.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 129785bad..070003972 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
+
 (** * Euclidean Division for integers, Euclid convention
 
     We use here the "usual" formulation of the Euclid Theorem
@@ -19,37 +21,29 @@
     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 : ZAxiomsSig')(Import DM : DivMod' Z).
- Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b.
-End ZDivSpecific.
 
-Module Type ZDiv (Z:ZAxiomsSig)
- := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
+    We simply extend NZDiv with a bound for modulo that holds
+    regardless of the sign of a and b. This new specification
+    subsume mod_bound_pos, which nonetheless stays there for
+    subtyping. Note also that ZAxiomSig now already contain
+    a div and a modulo (that follow the Floor convention).
+    We just ignore them here.
+*)
 
-Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
-Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
+Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A).
+ Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b.
+End EuclidSpec.
 
-Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
+Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z.
+Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z.
 
-(** We benefit from what already exists for NZ *)
+Module ZEuclidProp
+ (Import A : ZAxiomsSig')
+ (Import B : ZMulOrderProp A)
+ (Import C : ZSgnAbsProp A B)
+ (Import D : ZEuclid' A).
 
- 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 := Nop <+ NZDivProp Z ZD ZP.
+ Module Import NZDivP := Nop <+ NZDivProp A D B.
 
 (** Another formulation of the main equation *)
 
@@ -117,7 +111,7 @@ 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 abs_opp; now apply mod_always_pos.
 rewrite mul_opp_opp; now apply div_mod.
 Qed.
 
@@ -125,7 +119,7 @@ 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 abs_opp; now apply mod_always_pos.
 rewrite mul_opp_opp; now apply div_mod.
 Qed.
 
@@ -296,7 +290,7 @@ intros a b Hb.
 split.
 intros EQ.
 rewrite (div_mod a b Hb), EQ; nzsimpl.
-apply mod_always_pos.
+now apply mod_always_pos.
 intros. pos_or_neg b.
 apply div_small.
 now rewrite <- (abs_eq b).
@@ -365,7 +359,7 @@ intros.
 nzsimpl.
 rewrite (div_mod a b) at 1; try order.
 rewrite <- add_lt_mono_l.
-destruct (mod_always_pos a b).
+destruct (mod_always_pos a b). order.
 rewrite abs_eq in *; order.
 Qed.
 
@@ -375,7 +369,7 @@ 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).
+destruct (mod_always_pos a b). order.
 rewrite <- opp_pos_neg in Hb. rewrite abs_neq' in *; order.
 Qed.
 
@@ -469,7 +463,7 @@ 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.
+now apply mod_always_pos.
 (* equation *)
 rewrite (div_mod a b) at 1 by order.
 rewrite mul_add_distr_r.
@@ -566,7 +560,7 @@ Proof.
  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).
+ destruct (mod_always_pos (a/b) c), (mod_always_pos a b); try order.
  split.
  apply add_nonneg_nonneg; trivial.
  apply mul_nonneg_nonneg; order.
@@ -590,16 +584,15 @@ 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).
+ (a mod b == 0 <-> (b|a)).
 Proof.
 intros a b Hb. split.
-intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1.
+intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2.
  rewrite Hab; now nzsimpl.
 intros (c,Hc).
-rewrite Hc, mul_comm.
+rewrite <- Hc, mul_comm.
 now apply mod_mul.
 Qed.
 
-
-End ZDivProp.
+End ZEuclidProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index fd962024c..5f52f046f 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
+
 (** * Euclidean Division for integers (Floor convention)
 
     We use here the convention known as Floor, or Round-Toward-Bottom,
@@ -24,33 +26,13 @@
     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 := ZAxiomsSig <+ ZDiv.
-Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
-
-Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
+Module Type ZDivProp
+ (Import A : ZAxiomsSig')
+ (Import B : ZMulOrderProp A)
+ (Import C : ZSgnAbsProp A B).
 
 (** 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 := Nop <+ NZDivProp Z ZD ZP.
+Module Import NZDivP := Nop <+ NZDivProp A A B.
 
 (** Another formulation of the main equation *)
 
@@ -62,6 +44,18 @@ rewrite <- add_move_l.
 symmetry. now apply div_mod.
 Qed.
 
+(** We have a general bound for absolute values *)
+
+Lemma mod_bound_abs :
+ forall a b, b~=0 -> abs (a mod b) < abs b.
+Proof.
+intros.
+destruct (abs_spec b) as [(LE,EQ)|(LE,EQ)]; rewrite EQ.
+destruct (mod_pos_bound a b). order. now rewrite abs_eq.
+destruct (mod_neg_bound a b). order. rewrite abs_neq; trivial.
+now rewrite <- opp_lt_mono.
+Qed.
+
 (** Uniqueness theorems *)
 
 Theorem div_mod_unique : forall b q1 q2 r1 r2 : t,
@@ -230,11 +224,26 @@ 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] *)
+(** The sign of [a mod b] is the one of [b] (when it isn't null) *)
 
-(* TODO: a proper sgn function and theory *)
+Lemma mod_sign_nz : forall a b, b~=0 -> a mod b ~= 0 ->
+ sgn (a mod b) == sgn b.
+Proof.
+intros a b Hb H. destruct (lt_ge_cases 0 b) as [Hb'|Hb'].
+destruct (mod_pos_bound a b Hb'). rewrite 2 sgn_pos; order.
+destruct (mod_neg_bound a b). order. rewrite 2 sgn_neg; order.
+Qed.
+
+Lemma mod_sign : forall a b, b~=0 -> sgn (a mod b) ~= -sgn b.
+Proof.
+intros a b Hb H.
+destruct (eq_decidable (a mod b) 0) as [EQ|NEQ].
+apply Hb, sgn_null_iff, opp_inj. now rewrite <- H, opp_0, EQ, sgn_0.
+apply Hb, sgn_null_iff. apply eq_mul_0_l with 2; try order'. nzsimpl'.
+apply add_move_0_l. rewrite <- H. symmetry. now apply mod_sign_nz.
+Qed.
 
-Lemma mod_sign : forall a b, b~=0 -> (0 <= (a mod b) * b).
+Lemma mod_sign_mul : 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.
@@ -615,18 +624,5 @@ 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 ZDivProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 4ca692d00..37a0057ed 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
+
 (** * Euclidean Division for integers (Trunc convention)
 
     We use here the convention known as Trunc, or Round-Toward-Zero,
@@ -24,25 +26,23 @@
     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 := ZAxiomsSig <+ ZDiv.
-Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
-
-Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
+Module Type ZQuotProp
+ (Import A : ZAxiomsSig')
+ (Import B : ZMulOrderProp A)
+ (Import C : ZSgnAbsProp A B).
 
 (** We benefit from what already exists for NZ *)
 
- Module Import NZDivP := Nop <+ NZDivProp Z Z ZP.
+ Module Quot2Div <: NZDiv A.
+  Definition div := quot.
+  Definition modulo := remainder.
+  Definition div_wd := quot_wd.
+  Definition mod_wd := rem_wd.
+  Definition div_mod := quot_rem.
+  Definition mod_bound_pos := rem_bound_pos.
+ End Quot2Div.
+
+ Module NZQuot := Nop <+ NZDivProp A Quot2Div B.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
@@ -51,175 +51,269 @@ Ltac pos_or_neg a :=
 
 (** Another formulation of the main equation *)
 
-Lemma mod_eq :
- forall a b, b~=0 -> a mod b == a - b*(a/b).
+Lemma rem_eq :
+ forall a b, b~=0 -> a rem b == a - b*(a÷b).
 Proof.
 intros.
 rewrite <- add_move_l.
-symmetry. now apply div_mod.
+symmetry. now apply quot_rem.
 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 rem_opp_opp : forall a b, b ~= 0 -> (-a) rem (-b) == - (a rem b).
+Proof. intros. now rewrite rem_opp_r, rem_opp_l. Qed.
 
-Lemma div_opp_l : forall a b, b ~= 0 -> (-a)/b == -(a/b).
+Lemma quot_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.
+rewrite <- (add_cancel_r _ _ ((-a) rem b)).
+now rewrite <- quot_rem, rem_opp_l, mul_opp_r, <- opp_add_distr, <- quot_rem.
 Qed.
 
-Lemma div_opp_r : forall a b, b ~= 0 -> a/(-b) == -(a/b).
+Lemma quot_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.
+rewrite <- (add_cancel_r _ _ (a rem (-b))).
+now rewrite <- quot_rem, rem_opp_r, mul_opp_opp, <- quot_rem.
 Qed.
 
+Lemma quot_opp_opp : forall a b, b ~= 0 -> (-a)÷(-b) == a÷b.
+Proof. intros. now rewrite quot_opp_r, quot_opp_l, opp_involutive. Qed.
 
 (** Uniqueness theorems *)
 
-Theorem div_mod_unique : forall b q1 q2 r1 r2 : t,
+Theorem quot_rem_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.
+apply NZQuot.div_mod_unique with b; trivial.
 rewrite <- (opp_inj_wd r1 r2).
-apply div_mod_unique with (-b); trivial.
+apply NZQuot.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 quot_unique:
+ forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a÷b.
+Proof. intros; now apply NZQuot.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.
+Theorem rem_unique:
+ forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a rem b.
+Proof. intros; now apply NZQuot.mod_unique with q. Qed.
 
 (** A division by itself returns 1 *)
 
-Lemma div_same : forall a, a~=0 -> a/a == 1.
+Lemma quot_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.
+intros. pos_or_neg a. apply NZQuot.div_same; order.
+rewrite <- quot_opp_opp by trivial. now apply NZQuot.div_same.
 Qed.
 
-Lemma mod_same : forall a, a~=0 -> a mod a == 0.
+Lemma rem_same : forall a, a~=0 -> a rem a == 0.
 Proof.
-intros. rewrite mod_eq, div_same by trivial. nzsimpl. apply sub_diag.
+intros. rewrite rem_eq, quot_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.
+Theorem quot_small: forall a b, 0<=a<b -> a÷b == 0.
+Proof. exact NZQuot.div_small. Qed.
 
-(** Same situation, in term of modulo: *)
+(** Same situation, in term of remulo: *)
 
-Theorem mod_small: forall a b, 0<=a<b -> a mod b == a.
-Proof. exact mod_small. Qed.
+Theorem rem_small: forall a b, 0<=a<b -> a rem b == a.
+Proof. exact NZQuot.mod_small. Qed.
 
 (** * Basic values of divisions and modulo. *)
 
-Lemma div_0_l: forall a, a~=0 -> 0/a == 0.
+Lemma quot_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.
+intros. pos_or_neg a. apply NZQuot.div_0_l; order.
+rewrite <- quot_opp_opp, opp_0 by trivial. now apply NZQuot.div_0_l.
 Qed.
 
-Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0.
+Lemma rem_0_l: forall a, a~=0 -> 0 rem a == 0.
 Proof.
-intros; rewrite mod_eq, div_0_l; now nzsimpl.
+intros; rewrite rem_eq, quot_0_l; now nzsimpl.
 Qed.
 
-Lemma div_1_r: forall a, a/1 == a.
+Lemma quot_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.
+intros. pos_or_neg a. now apply NZQuot.div_1_r.
+apply opp_inj. rewrite <- quot_opp_l. apply NZQuot.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.
+Lemma rem_1_r: forall a, a rem 1 == 0.
 Proof.
-intros. rewrite mod_eq, div_1_r; nzsimpl; auto using sub_diag.
+intros. rewrite rem_eq, quot_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 quot_1_l: forall a, 1<a -> 1÷a == 0.
+Proof. exact NZQuot.div_1_l. Qed.
+
+Lemma rem_1_l: forall a, 1<a -> 1 rem a == 1.
+Proof. exact NZQuot.mod_1_l. Qed.
+
+Lemma quot_mul : forall a b, b~=0 -> (a*b)÷b == a.
+Proof.
+intros. pos_or_neg a; pos_or_neg b. apply NZQuot.div_mul; order.
+rewrite <- quot_opp_opp, <- mul_opp_r by order. apply NZQuot.div_mul; order.
+rewrite <- opp_inj_wd, <- quot_opp_l, <- mul_opp_l by order.
+apply NZQuot.div_mul; order.
+rewrite <- opp_inj_wd, <- quot_opp_r, <- mul_opp_opp by order.
+apply NZQuot.div_mul; order.
+Qed.
+
+Lemma rem_mul : forall a b, b~=0 -> (a*b) rem b == 0.
+Proof.
+intros. rewrite rem_eq, quot_mul by trivial. rewrite mul_comm; apply sub_diag.
+Qed.
+
+(** The sign of [a rem b] is the one of [a] (when it's not null) *)
+
+Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b.
+Proof.
+ intros. pos_or_neg b. destruct (rem_bound_pos a b); order.
+ rewrite <- rem_opp_r; trivial.
+ destruct (rem_bound_pos a (-b)); trivial.
+Qed.
+
+Lemma rem_nonpos : forall a b, b~=0 -> a <= 0 -> a rem b <= 0.
+Proof.
+ intros a b Hb Ha.
+ apply opp_nonneg_nonpos. apply opp_nonneg_nonpos in Ha.
+ rewrite <- rem_opp_l by trivial. now apply rem_nonneg.
+Qed.
 
-Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
-Proof. exact mod_1_l. Qed.
+Lemma rem_sign_mul : forall a b, b~=0 -> 0 <= (a rem b) * a.
+Proof.
+intros a b Hb. destruct (le_ge_cases 0 a).
+ apply mul_nonneg_nonneg; trivial. now apply rem_nonneg.
+ apply mul_nonpos_nonpos; trivial. now apply rem_nonpos.
+Qed.
 
-Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a.
+Lemma rem_sign_nz : forall a b, b~=0 -> a rem b ~= 0 ->
+ sgn (a rem b) == sgn 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.
+intros a b Hb H. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]].
+rewrite 2 sgn_pos; try easy.
+ generalize (rem_nonneg a b Hb (lt_le_incl _ _ LT)). order.
+now rewrite <- EQ, rem_0_l, sgn_0.
+rewrite 2 sgn_neg; try easy.
+ generalize (rem_nonpos a b Hb (lt_le_incl _ _ LT)). order.
 Qed.
 
-Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0.
+Lemma rem_sign : forall a b, a~=0 -> b~=0 -> sgn (a rem b) ~= -sgn a.
 Proof.
-intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
+intros a b Ha Hb H.
+destruct (eq_decidable (a rem b) 0) as [EQ|NEQ].
+apply Ha, sgn_null_iff, opp_inj. now rewrite <- H, opp_0, EQ, sgn_0.
+apply Ha, sgn_null_iff. apply eq_mul_0_l with 2; try order'. nzsimpl'.
+apply add_move_0_l. rewrite <- H. symmetry. now apply rem_sign_nz.
 Qed.
 
-(** * Order results about mod and div *)
+(** Operations and absolute value *)
+
+Lemma rem_abs_l : forall a b, b ~= 0 -> (abs a) rem b == abs (a rem b).
+Proof.
+intros a b Hb. destruct (le_ge_cases 0 a) as [LE|LE].
+rewrite 2 abs_eq; try easy. now apply rem_nonneg.
+rewrite 2 abs_neq, rem_opp_l; try easy. now apply rem_nonpos.
+Qed.
+
+Lemma rem_abs_r : forall a b, b ~= 0 -> a rem (abs b) == a rem b.
+Proof.
+intros a b Hb. destruct (le_ge_cases 0 b).
+now rewrite abs_eq. now rewrite abs_neq, ?rem_opp_r.
+Qed.
+
+Lemma rem_abs : forall a b,  b ~= 0 -> (abs a) rem (abs b) == abs (a rem b).
+Proof.
+intros. now rewrite rem_abs_r, rem_abs_l.
+Qed.
+
+Lemma quot_abs_l : forall a b, b ~= 0 -> (abs a)÷b == (sgn a)*(a÷b).
+Proof.
+intros a b Hb. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]].
+rewrite abs_eq, sgn_pos by order. now nzsimpl.
+rewrite <- EQ, abs_0, quot_0_l; trivial. now nzsimpl.
+rewrite abs_neq, quot_opp_l, sgn_neg by order.
+ rewrite mul_opp_l. now nzsimpl.
+Qed.
+
+Lemma quot_abs_r : forall a b, b ~= 0 -> a÷(abs b) == (sgn b)*(a÷b).
+Proof.
+intros a b Hb. destruct (lt_trichotomy 0 b) as [LT|[EQ|LT]].
+rewrite abs_eq, sgn_pos by order. now nzsimpl.
+order.
+rewrite abs_neq, quot_opp_r, sgn_neg by order.
+ rewrite mul_opp_l. now nzsimpl.
+Qed.
+
+Lemma quot_abs : forall a b, b ~= 0 -> (abs a)÷(abs b) == abs (a÷b).
+Proof.
+intros a b Hb.
+pos_or_neg a; [rewrite (abs_eq a)|rewrite (abs_neq a)];
+ try apply opp_nonneg_nonpos; try order.
+pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)];
+ try apply opp_nonneg_nonpos; try order.
+rewrite abs_eq; try easy. apply NZQuot.div_pos; order.
+rewrite <- abs_opp, <- quot_opp_r, abs_eq; try easy.
+ apply NZQuot.div_pos; order.
+pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)];
+ try apply opp_nonneg_nonpos; try order.
+rewrite <- (abs_opp (_÷_)), <- quot_opp_l, abs_eq; try easy.
+ apply NZQuot.div_pos; order.
+rewrite <- (quot_opp_opp a b), abs_eq; try easy.
+ apply NZQuot.div_pos; order.
+Qed.
+
+(** We have a general bound for absolute values *)
+
+Lemma rem_bound_abs :
+ forall a b, b~=0 -> abs (a rem b) < abs b.
+Proof.
+intros. rewrite <- rem_abs; trivial.
+apply rem_bound_pos. apply abs_nonneg. now apply abs_pos.
+Qed.
+
+(** * Order results about rem and quot *)
 
 (** 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 rem_le: forall a b, 0<=a -> 0<b -> a rem b <= a.
+Proof. exact NZQuot.mod_le. Qed.
 
-Theorem div_pos : forall a b, 0<=a -> 0<b -> 0<= a/b.
-Proof. exact div_pos. Qed.
+Theorem quot_pos : forall a b, 0<=a -> 0<b -> 0<= a÷b.
+Proof. exact NZQuot.div_pos. Qed.
 
-Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b.
-Proof. exact div_str_pos. Qed.
+Lemma quot_str_pos : forall a b, 0<b<=a -> 0 < a÷b.
+Proof. exact NZQuot.div_str_pos. Qed.
 
-Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> abs a < abs b).
+Lemma quot_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 NZQuot.div_small_iff; try order. rewrite 2 abs_eq; intuition; order.
+rewrite <- opp_inj_wd, opp_0, <- quot_opp_r, NZQuot.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 <- opp_inj_wd, opp_0, <- quot_opp_l, NZQuot.div_small_iff by order.
  rewrite (abs_neq' a), (abs_eq b); intuition; order.
-rewrite <- div_opp_opp, div_small_iff by order.
+rewrite <- quot_opp_opp, NZQuot.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).
+Lemma rem_small_iff : forall a b, b~=0 -> (a rem b == a <-> abs a < abs b).
 Proof.
-intros. rewrite mod_eq, <- div_small_iff by order.
+intros. rewrite rem_eq, <- quot_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.
@@ -227,306 +321,295 @@ 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.
+Lemma quot_lt : forall a b, 0<a -> 1<b -> a÷b < a.
+Proof. exact NZQuot.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.
+Lemma quot_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.
+intros. pos_or_neg a. apply NZQuot.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.
+ rewrite <- opp_nonneg_nonpos, <- quot_opp_l by order.
+ apply quot_pos; order.
+ apply quot_pos; order.
+rewrite opp_le_mono in *. rewrite <- 2 quot_opp_l by order.
+ apply NZQuot.div_le_mono; intuition; order.
 Qed.
 
 (** With this choice of division,
-    rounding of div is always done toward zero: *)
+    rounding of quot is always done toward zero: *)
 
-Lemma mul_div_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a/b) <= a.
+Lemma mul_quot_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.
+apply mul_nonneg_nonneg; [|apply quot_pos]; order.
+apply NZQuot.mul_div_le; order.
+rewrite <- mul_opp_opp, <- quot_opp_r by order.
 split.
-apply mul_nonneg_nonneg; [|apply div_pos]; order.
-apply mul_div_le; order.
+apply mul_nonneg_nonneg; [|apply quot_pos]; order.
+apply NZQuot.mul_div_le; order.
 Qed.
 
-Lemma mul_div_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a/b) <= 0.
+Lemma mul_quot_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, opp_le_mono, <-mul_opp_r, <-quot_opp_l by order.
 rewrite <- opp_nonneg_nonpos in *.
-destruct (mul_div_le (-a) b); tauto.
+destruct (mul_quot_le (-a) b); tauto.
 Qed.
 
-(** For positive numbers, considering [S (a/b)] leads to an upper bound for [a] *)
+(** 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.
+Lemma mul_succ_quot_gt: forall a b, 0<=a -> 0<b -> a < b*(S (a÷b)).
+Proof. exact NZQuot.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.
+Lemma mul_pred_quot_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_lt_mono, <- mul_opp_r, opp_pred, <- quot_opp_l by order.
 rewrite <- opp_nonneg_nonpos in *.
-now apply mul_succ_div_gt.
+now apply mul_succ_quot_gt.
 Qed.
 
-Lemma mul_pred_div_gt: forall a b, 0<=a -> b<0 -> a < b*(P (a/b)).
+Lemma mul_pred_quot_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 <- mul_opp_opp, opp_pred, <- quot_opp_r by order.
 rewrite <- opp_pos_neg in *.
-now apply mul_succ_div_gt.
+now apply mul_succ_quot_gt.
 Qed.
 
-Lemma mul_succ_div_lt: forall a b, a<=0 -> b<0 -> b*(S (a/b)) < a.
+Lemma mul_succ_quot_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_lt_mono, <- mul_opp_l, <- quot_opp_opp by order.
 rewrite <- opp_nonneg_nonpos, <- opp_pos_neg in *.
-now apply mul_succ_div_gt.
+now apply mul_succ_quot_gt.
 Qed.
 
-(** Inequality [mul_div_le] is exact iff the modulo is zero. *)
+(** Inequality [mul_quot_le] is exact iff the modulo is zero. *)
 
-Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0).
+Lemma quot_exact : forall a b, b~=0 -> (a == b*(a÷b) <-> a rem b == 0).
 Proof.
-intros. rewrite mod_eq by order. rewrite sub_move_r; nzsimpl; tauto.
+intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additionnal inequalities about quot. *)
 
-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 quot_lt_upper_bound:
+  forall a b q, 0<=a -> 0<b -> a < b*q -> a÷b < q.
+Proof. exact NZQuot.div_lt_upper_bound. Qed.
 
-Theorem div_le_upper_bound:
-  forall a b q, 0<b -> a <= b*q -> a/b <= q.
+Theorem quot_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.
+rewrite <- (quot_mul q b) by order.
+apply quot_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.
+Theorem quot_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.
+rewrite <- (quot_mul q b) by order.
+apply quot_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.
+Lemma quot_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p÷r <= p÷q.
+Proof. exact NZQuot.div_le_compat_l. Qed.
 
-(** * Relations between usual operations and mod and div *)
+(** * Relations between usual operations and rem and quot *)
 
 (** 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] *)
+    [(a+b*c) rem c <> a rem 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.
+Lemma rem_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a ->
+ (a + b * c) rem c == a rem 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.
+assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) rem c == a rem c).
+ intros. pos_or_neg c. apply NZQuot.mod_add; order.
+ rewrite <- (rem_opp_r a), <- (rem_opp_r (a+b*c)) by order.
  rewrite <- mul_opp_opp in *.
- apply mod_add; order.
+ apply NZQuot.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.
+rewrite <- 2 rem_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.
+Lemma quot_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.
+rewrite <- (add_cancel_r _ _ ((a+b*c) rem c)).
+rewrite <- quot_rem, rem_add by trivial.
+now rewrite mul_add_distr_l, add_shuffle0, <-quot_rem, 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.
+Lemma quot_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.
+ intros a b c. rewrite add_comm, (add_comm a). now apply quot_add.
 Qed.
 
 (** Cancellations. *)
 
-Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 ->
- (a*c)/(b*c) == a/b.
+Lemma quot_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.
+assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)÷(b*c) == a÷b).
+ intros. pos_or_neg c. apply NZQuot.div_mul_cancel_r; order.
+ rewrite <- quot_opp_opp, <- 2 mul_opp_r. apply NZQuot.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).
+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.
+ apply opp_inj. rewrite <- 2 quot_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.
+apply opp_inj. rewrite <- 2 quot_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.
+Lemma quot_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.
+intros. rewrite !(mul_comm c); now apply quot_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.
+Lemma mul_rem_distr_r: forall a b c, b~=0 -> c~=0 ->
+  (a*c) rem (b*c) == (a rem 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).
+rewrite ! rem_eq by trivial.
+rewrite quot_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).
+Lemma mul_rem_distr_l: forall a b c, b~=0 -> c~=0 ->
+  (c*a) rem (c*b) == c * (a rem b).
 Proof.
-intros; rewrite !(mul_comm c); now apply mul_mod_distr_r.
+intros; rewrite !(mul_comm c); now apply mul_rem_distr_r.
 Qed.
 
 (** Operations modulo. *)
 
-Theorem mod_mod: forall a n, n~=0 ->
- (a mod n) mod n == a mod n.
+Theorem rem_rem: forall a n, n~=0 ->
+ (a rem n) rem n == a rem 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.
+intros. pos_or_neg a; pos_or_neg n. apply NZQuot.mod_mod; order.
+rewrite <- ! (rem_opp_r _ n) by trivial. apply NZQuot.mod_mod; order.
+apply opp_inj. rewrite <- !rem_opp_l by order. apply NZQuot.mod_mod; order.
+apply opp_inj. rewrite <- !rem_opp_opp by order. apply NZQuot.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.
+Lemma mul_rem_idemp_l : forall a b n, n~=0 ->
+ ((a rem n)*b) rem n == (a*b) rem 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.
+         ((a rem n)*b) rem n == (a*b) rem n).
+ intros. pos_or_neg n. apply NZQuot.mul_mod_idemp_l; order.
+ rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.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).
+         ((a rem n)*b) rem n == (a*b) rem n).
  intros. pos_or_neg b. now apply Aux1.
- apply opp_inj. rewrite <-2 mod_opp_l, <-2 mul_opp_r by order.
+ apply opp_inj. rewrite <-2 rem_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 opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_l, <-rem_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.
+Lemma mul_rem_idemp_r : forall a b n, n~=0 ->
+ (a*(b rem n)) rem n == (a*b) rem n.
 Proof.
-intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l.
+intros. rewrite !(mul_comm a). now apply mul_rem_idemp_l.
 Qed.
 
-Theorem mul_mod: forall a b n, n~=0 ->
- (a * b) mod n == ((a mod n) * (b mod n)) mod n.
+Theorem mul_rem: forall a b n, n~=0 ->
+ (a * b) rem n == ((a rem n) * (b rem n)) rem n.
 Proof.
-intros. now rewrite mul_mod_idemp_l, mul_mod_idemp_r.
+intros. now rewrite mul_rem_idemp_l, mul_rem_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]
+       [(a+b) rem n = (a rem n + b rem n) rem n]
   for any a and b.
-  For instance, take (8 + (-10)) mod 3 = -2 whereas
-  (8 mod 3 + (-10 mod 3)) mod 3 = 1.
+  For instance, take (8 + (-10)) rem 3 = -2 whereas
+  (8 rem 3 + (-10 rem 3)) rem 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.
+Lemma add_rem_idemp_l : forall a b n, n~=0 -> 0 <= a*b ->
+ ((a rem n)+b) rem n == (a+b) rem 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.
+          ((a rem n)+b) rem n == (a+b) rem n).
+ intros. pos_or_neg n. apply NZQuot.add_mod_idemp_l; order.
+ rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.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.
+apply opp_inj. rewrite <-2 rem_opp_l, 2 opp_add_distr, <-rem_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.
+Lemma add_rem_idemp_r : forall a b n, n~=0 -> 0 <= a*b ->
+ (a+(b rem n)) rem n == (a+b) rem n.
 Proof.
-intros. rewrite !(add_comm a). apply add_mod_idemp_l; trivial.
+intros. rewrite !(add_comm a). apply add_rem_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.
+Theorem add_rem: forall a b n, n~=0 -> 0 <= a*b ->
+ (a+b) rem n == (a rem n + b rem n) rem n.
 Proof.
-intros a b n Hn Hab. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial.
+intros a b n Hn Hab. rewrite add_rem_idemp_l, add_rem_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)];
+ destruct (le_0_mul _ _ (rem_sign_mul 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.
+ setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order.
+ setoid_replace b with 0 by order. rewrite rem_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).
+Lemma quot_quot : 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.
+assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a÷b)÷c == a÷(b*c)).
+ intros. pos_or_neg c. apply NZQuot.div_div; order.
+ apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_r; trivial.
+ apply NZQuot.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)).
+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 opp_inj. rewrite <- quot_opp_l, <- 2 quot_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.
+apply opp_inj. rewrite <- 3 quot_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.
+Theorem quot_mul_le:
+ forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a÷b) <= (c*a)÷b.
+Proof. exact NZQuot.div_mul_le. Qed.
 
-End ZDivProp.
+End ZQuotProp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
index d58d1f1e2..6b1d4675e 100644
--- a/theories/Numbers/Integer/Abstract/ZGcd.v
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -10,10 +10,10 @@
 
 Require Import ZAxioms ZMulOrder ZSgnAbs NZGcd.
 
-Module ZGcdProp
+Module Type ZGcdProp
  (Import A : ZAxiomsSig')
  (Import B : ZMulOrderProp A)
- (Import D : ZSgnAbsProp A B).
+ (Import C : ZSgnAbsProp A B).
 
  Include NZGcdProp A A B.
 
@@ -269,8 +269,6 @@ Proof.
  symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order.
 Qed.
 
-(** TODO : relation between gcd and division and modulo *)
-
 (** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *)
 
 End ZGcdProp.
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
new file mode 100644
index 000000000..27bd5962c
--- /dev/null
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -0,0 +1,436 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor.
+
+(** * Least Common Multiple *)
+
+(** Unlike other functions around, we will define lcm below instead of
+  axiomatizing it. Indeed, there is no "prior art" about lcm in the
+  standard library to be compliant with, and the generic definition
+  of lcm via gcd is quite reasonable.
+
+  By the way, we also state here some combined properties of div/mod
+  and quot/rem and gcd.
+*)
+
+Module Type ZLcmProp
+ (Import A : ZAxiomsSig')
+ (Import B : ZMulOrderProp A)
+ (Import C : ZSgnAbsProp A B)
+ (Import D : ZDivProp A B C)
+ (Import E : ZQuotProp A B C)
+ (Import F : ZGcdProp A B C).
+
+(** The two notions of division are equal on non-negative numbers *)
+
+Lemma quot_div_nonneg : forall a b, 0<=a -> 0<b -> a÷b == a/b.
+Proof.
+ intros. apply div_unique_pos with (a rem b).
+ now apply rem_bound_pos.
+ apply quot_rem. order.
+Qed.
+
+Lemma rem_mod_nonneg : forall a b, 0<=a -> 0<b -> a rem b == a mod b.
+Proof.
+ intros. apply mod_unique_pos with (a÷b).
+ now apply rem_bound_pos.
+ apply quot_rem. order.
+Qed.
+
+(** Modulo and remainder are null at the same place,
+    and this correspond to the divisibility relation. *)
+
+Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)).
+Proof.
+ intros a b Hb. split.
+ intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 2.
+  rewrite Hab; now nzsimpl.
+ intros (c,Hc). rewrite <- Hc, mul_comm. now apply mod_mul.
+Qed.
+
+Lemma rem_divide : forall a b, b~=0 -> (a rem b == 0 <-> (b|a)).
+Proof.
+ intros a b Hb. split.
+ intros Hab. exists (a÷b). rewrite (quot_rem a b Hb) at 2.
+  rewrite Hab; now nzsimpl.
+ intros (c,Hc). rewrite <- Hc, mul_comm. now apply rem_mul.
+Qed.
+
+Lemma rem_mod_eq_0 : forall a b, b~=0 -> (a rem b == 0 <-> a mod b == 0).
+Proof.
+ intros a b Hb. now rewrite mod_divide, rem_divide.
+Qed.
+
+(** When division is exact, div and quot agree *)
+
+Lemma quot_div_exact : forall a b, b~=0 -> (b|a) -> a÷b == a/b.
+Proof.
+ intros a b Hb H.
+ apply mul_cancel_l with b; trivial.
+ assert (H':=H).
+ apply rem_divide, quot_exact in H; trivial.
+ apply mod_divide, div_exact in H'; trivial.
+ now rewrite <-H,<-H'.
+Qed.
+
+Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) ->
+ (c*a)/b == c*(a/b).
+Proof.
+ intros a b c Hb H.
+ apply mul_cancel_l with b; trivial.
+ rewrite mul_assoc, mul_shuffle0.
+ assert (H':=H). apply mod_divide, div_exact in H'; trivial.
+ rewrite <- H', (mul_comm a c).
+ symmetry. apply div_exact; trivial.
+ apply mod_divide; trivial.
+ now apply divide_mul_r.
+Qed.
+
+Lemma divide_quot_mul_exact : forall a b c, b~=0 -> (b|a) ->
+ (c*a)÷b == c*(a÷b).
+Proof.
+ intros a b c Hb H.
+ rewrite 2 quot_div_exact; trivial.
+ apply divide_div_mul_exact; trivial.
+ now apply divide_mul_r.
+Qed.
+
+(** Gcd of divided elements, for exact divisions *)
+
+Lemma gcd_div_factor : forall a b c, 0<c -> (c|a) -> (c|b) ->
+ gcd (a/c) (b/c) == (gcd a b)/c.
+Proof.
+ intros a b c Hc Ha Hb.
+ apply mul_cancel_l with c; try order.
+ assert (H:=gcd_greatest _ _ _ Ha Hb).
+ apply mod_divide, div_exact in H; try order.
+ rewrite <- H.
+ rewrite <- gcd_mul_mono_l_nonneg; try order.
+ apply gcd_wd; symmetry; apply div_exact; try order;
+  apply mod_divide; trivial; try order.
+Qed.
+
+Lemma gcd_quot_factor : forall a b c, 0<c -> (c|a) -> (c|b) ->
+ gcd (a÷c) (b÷c) == (gcd a b)÷c.
+Proof.
+ intros a b c Hc Ha Hb. rewrite !quot_div_exact; trivial; try order.
+ now apply gcd_div_factor. now apply gcd_greatest.
+Qed.
+
+Lemma gcd_div_gcd : forall a b g, g~=0 -> g == gcd a b ->
+ gcd (a/g) (b/g) == 1.
+Proof.
+ intros a b g NZ EQ. rewrite gcd_div_factor.
+ now rewrite <- EQ, div_same.
+ generalize (gcd_nonneg a b); order.
+ rewrite EQ; apply gcd_divide_l.
+ rewrite EQ; apply gcd_divide_r.
+Qed.
+
+Lemma gcd_quot_gcd : forall a b g, g~=0 -> g == gcd a b ->
+ gcd (a÷g) (b÷g) == 1.
+Proof.
+ intros a b g NZ EQ. rewrite !quot_div_exact; trivial.
+ now apply gcd_div_gcd.
+ rewrite EQ; apply gcd_divide_r.
+ rewrite EQ; apply gcd_divide_l.
+Qed.
+
+(** The following equality is crucial for Euclid algorithm *)
+
+Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a.
+Proof.
+ intros a b Hb. rewrite mod_eq; trivial.
+ rewrite <- add_opp_r, mul_comm, <- mul_opp_l.
+ rewrite (gcd_comm _ b).
+ apply gcd_add_mult_diag_r.
+Qed.
+
+Lemma gcd_rem : forall a b, b~=0 -> gcd (a rem b) b == gcd b a.
+Proof.
+ intros a b Hb. rewrite rem_eq; trivial.
+ rewrite <- add_opp_r, mul_comm, <- mul_opp_l.
+ rewrite (gcd_comm _ b).
+ apply gcd_add_mult_diag_r.
+Qed.
+
+(** We now define lcm thanks to gcd:
+
+    lcm a b = a * (b / gcd a b)
+            = (a / gcd a b) * b
+            = (a*b) / gcd a b
+
+   We had an abs in order to have an always-nonnegative lcm,
+   in the spirit of gcd. Nota: [lcm 0 0] should be 0, which
+   isn't garantee with the third equation above.
+*)
+
+Definition lcm a b := abs (a*(b/gcd a b)).
+
+Instance lcm_wd : Proper (eq==>eq==>eq) lcm.
+Proof.
+ unfold lcm. intros x x' Hx y y' Hy. now rewrite Hx, Hy.
+Qed.
+
+Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 ->
+  a * (b / gcd a b) == (a*b)/gcd a b.
+Proof.
+ intros a b H. rewrite divide_div_mul_exact; try easy. apply gcd_divide_r.
+Qed.
+
+Lemma lcm_equiv2 : forall a b, gcd a b ~= 0 ->
+  (a / gcd a b) * b == (a*b)/gcd a b.
+Proof.
+ intros a b H. rewrite 2 (mul_comm _ b).
+ rewrite divide_div_mul_exact; try easy. apply gcd_divide_l.
+Qed.
+
+Lemma gcd_div_swap : forall a b,
+ (a / gcd a b) * b == a * (b / gcd a b).
+Proof.
+ intros a b. destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ].
+ apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ, EQ'. now nzsimpl.
+ now rewrite lcm_equiv1, <-lcm_equiv2.
+Qed.
+
+Lemma divide_lcm_l : forall a b, (a | lcm a b).
+Proof.
+ unfold lcm. intros a b. apply divide_abs_r, divide_factor_l.
+Qed.
+
+Lemma divide_lcm_r : forall a b, (b | lcm a b).
+Proof.
+ unfold lcm. intros a b. apply divide_abs_r. rewrite <- gcd_div_swap.
+ apply divide_factor_r.
+Qed.
+
+Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a).
+Proof.
+ intros a b c Ha Hb (c',Hc). exists c'.
+ now rewrite mul_comm, <- divide_div_mul_exact, mul_comm, Hc.
+Qed.
+
+Lemma lcm_least : forall a b c,
+ (a | c) -> (b | c) -> (lcm a b | c).
+Proof.
+ intros a b c Ha Hb. unfold lcm. apply divide_abs_l.
+ destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ].
+ apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ in *. now nzsimpl.
+ assert (Ga := gcd_divide_l a b).
+ assert (Gb := gcd_divide_r a b).
+ set (g:=gcd a b) in *.
+ assert (Ha' := divide_div g a c NEQ Ga Ha).
+ assert (Hb' := divide_div g b c NEQ Gb Hb).
+ destruct Ha' as (a',Ha'). rewrite <- Ha' in Hb'.
+ apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm].
+ destruct Hb' as (b',Hb').
+ exists b'.
+ rewrite <- mul_assoc, Hb'.
+ rewrite (proj2 (div_exact c g NEQ)).
+ rewrite <- Ha', mul_assoc. apply mul_wd; try easy.
+ apply div_exact; trivial.
+ apply mod_divide; trivial.
+ apply mod_divide; trivial. transitivity a; trivial.
+Qed.
+
+Lemma lcm_nonneg : forall a b, 0 <= lcm a b.
+Proof.
+ intros a b. unfold lcm. apply abs_nonneg.
+Qed.
+
+Lemma lcm_comm : forall a b, lcm a b == lcm b a.
+Proof.
+ intros a b. unfold lcm. rewrite (gcd_comm b), (mul_comm b).
+ now rewrite <- gcd_div_swap.
+Qed.
+
+Lemma lcm_divide_iff : forall n m p,
+  (lcm n m | p) <-> (n | p) /\ (m | p).
+Proof.
+ intros. split. split.
+ transitivity (lcm n m); trivial using divide_lcm_l.
+ transitivity (lcm n m); trivial using divide_lcm_r.
+ intros (H,H'). now apply lcm_least.
+Qed.
+
+Lemma lcm_unique : forall n m p,
+ 0<=p -> (n|p) -> (m|p) ->
+ (forall q, (n|q) -> (m|q) -> (p|q)) ->
+ lcm n m == p.
+Proof.
+ intros n m p Hp Hn Hm H.
+ apply divide_antisym_nonneg; trivial. apply lcm_nonneg.
+ now apply lcm_least.
+ apply H. apply divide_lcm_l. apply divide_lcm_r.
+Qed.
+
+Lemma lcm_unique_alt : forall n m p, 0<=p ->
+ (forall q, (p|q) <-> (n|q) /\ (m|q)) ->
+ lcm n m == p.
+Proof.
+ intros n m p Hp H.
+ apply lcm_unique; trivial.
+ apply -> H. apply divide_refl.
+ apply -> H. apply divide_refl.
+ intros. apply H. now split.
+Qed.
+
+Lemma lcm_assoc : forall n m p, lcm n (lcm m p) == lcm (lcm n m) p.
+Proof.
+ intros. apply lcm_unique_alt; try apply lcm_nonneg.
+ intros. now rewrite !lcm_divide_iff, and_assoc.
+Qed.
+
+Lemma lcm_0_l : forall n, lcm 0 n == 0.
+Proof.
+ intros. apply lcm_unique; trivial. order.
+ apply divide_refl.
+ apply divide_0_r.
+Qed.
+
+Lemma lcm_0_r : forall n, lcm n 0 == 0.
+Proof.
+ intros. now rewrite lcm_comm, lcm_0_l.
+Qed.
+
+Lemma lcm_1_l_nonneg : forall n, 0<=n -> lcm 1 n == n.
+Proof.
+ intros. apply lcm_unique; trivial using divide_1_l, le_0_1, divide_refl.
+Qed.
+
+Lemma lcm_1_r_nonneg : forall n, 0<=n -> lcm n 1 == n.
+Proof.
+ intros. now rewrite lcm_comm, lcm_1_l_nonneg.
+Qed.
+
+Lemma lcm_diag_nonneg : forall n, 0<=n -> lcm n n == n.
+Proof.
+ intros. apply lcm_unique; trivial using divide_refl.
+Qed.
+
+Lemma lcm_eq_0 : forall n m, lcm n m == 0 <-> n == 0 \/ m == 0.
+Proof.
+ intros. split.
+ intros EQ.
+ apply eq_mul_0.
+ apply divide_0_l. rewrite <- EQ. apply lcm_least.
+  apply divide_factor_l. apply divide_factor_r.
+ destruct 1 as [EQ|EQ]; rewrite EQ. apply lcm_0_l. apply lcm_0_r.
+Qed.
+
+Lemma divide_lcm_eq_r : forall n m, 0<=m -> (n|m) -> lcm n m == m.
+Proof.
+ intros n m Hm H. apply lcm_unique_alt; trivial.
+ intros q. split. split; trivial. now transitivity m.
+ now destruct 1.
+Qed.
+
+Lemma divide_lcm_iff : forall n m, 0<=m -> ((n|m) <-> lcm n m == m).
+Proof.
+ intros n m Hn. split. now apply divide_lcm_eq_r.
+ intros EQ. rewrite <- EQ. apply divide_lcm_l.
+Qed.
+
+Lemma lcm_opp_l : forall n m, lcm (-n) m == lcm n m.
+Proof.
+ intros. apply lcm_unique_alt; try apply lcm_nonneg.
+ intros. rewrite divide_opp_l. apply lcm_divide_iff.
+Qed.
+
+Lemma lcm_opp_r : forall n m, lcm n (-m) == lcm n m.
+Proof.
+ intros. now rewrite lcm_comm, lcm_opp_l, lcm_comm.
+Qed.
+
+Lemma lcm_abs_l : forall n m, lcm (abs n) m == lcm n m.
+Proof.
+ intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H.
+ easy. apply lcm_opp_l.
+Qed.
+
+Lemma lcm_abs_r : forall n m, lcm n (abs m) == lcm n m.
+Proof.
+ intros. now rewrite lcm_comm, lcm_abs_l, lcm_comm.
+Qed.
+
+Lemma lcm_1_l : forall n, lcm 1 n == abs n.
+Proof.
+ intros. rewrite <- lcm_abs_r. apply lcm_1_l_nonneg, abs_nonneg.
+Qed.
+
+Lemma lcm_1_r : forall n, lcm n 1 == abs n.
+Proof.
+ intros. now rewrite lcm_comm, lcm_1_l.
+Qed.
+
+Lemma lcm_diag : forall n, lcm n n == abs n.
+Proof.
+ intros. rewrite <- lcm_abs_l, <- lcm_abs_r.
+ apply lcm_diag_nonneg, abs_nonneg.
+Qed.
+
+Lemma lcm_mul_mono_l :
+  forall n m p, lcm (p * n) (p * m) == abs p * lcm n m.
+Proof.
+ intros n m p.
+ destruct (eq_decidable p 0) as [Hp|Hp].
+  rewrite Hp. nzsimpl. rewrite lcm_0_l, abs_0. now nzsimpl.
+ destruct (eq_decidable (gcd n m) 0) as [Hg|Hg].
+  apply gcd_eq_0 in Hg. destruct Hg as (Hn,Hm); rewrite Hn, Hm.
+  nzsimpl. rewrite lcm_0_l. now nzsimpl.
+ unfold lcm.
+ rewrite gcd_mul_mono_l.
+ rewrite !abs_mul, mul_assoc. apply mul_wd; try easy.
+ rewrite <- (abs_sgn p) at 1. rewrite <- mul_assoc.
+ rewrite div_mul_cancel_l; trivial.
+ rewrite divide_div_mul_exact; trivial. rewrite abs_mul.
+ rewrite <- (sgn_abs (sgn p)), sgn_sgn.
+ destruct (sgn_spec p) as [(_,EQ)|[(EQ,_)|(_,EQ)]].
+  rewrite EQ. now nzsimpl. order.
+  rewrite EQ. rewrite mul_opp_l, mul_opp_r, opp_involutive. now nzsimpl.
+ apply gcd_divide_r.
+ contradict Hp. now apply abs_0_iff.
+Qed.
+
+Lemma lcm_mul_mono_l_nonneg :
+ forall n m p, 0<=p -> lcm (p*n) (p*m) == p * lcm n m.
+Proof.
+ intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_l.
+Qed.
+
+Lemma lcm_mul_mono_r :
+ forall n m p, lcm (n * p) (m * p) == lcm n m * abs p.
+Proof.
+ intros n m p. now rewrite !(mul_comm _ p), lcm_mul_mono_l, mul_comm.
+Qed.
+
+Lemma lcm_mul_mono_r_nonneg :
+ forall n m p, 0<=p -> lcm (n*p) (m*p) == lcm n m * p.
+Proof.
+ intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_r.
+Qed.
+
+Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 ->
+ (gcd n m == 1 <-> lcm n m == abs (n*m)).
+Proof.
+ intros n m Hn Hm. split; intros H.
+ unfold lcm. rewrite H. now rewrite div_1_r.
+ unfold lcm in *.
+ rewrite !abs_mul in H. apply mul_cancel_l in H; [|now rewrite abs_0_iff].
+ assert (H' := gcd_divide_r n m).
+ assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order).
+ apply mod_divide in H'; trivial. apply div_exact in H'; trivial.
+ assert (m / gcd n m ~=0) by (contradict Hm; rewrite H', Hm; now nzsimpl).
+ rewrite <- (mul_1_l (abs (_/_))) in H.
+ rewrite H' in H at 3. rewrite abs_mul in H.
+ apply mul_cancel_r in H; [|now rewrite abs_0_iff].
+ rewrite abs_eq in H. order. apply gcd_nonneg.
+Qed.
+
+End ZLcmProp.
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 6fbf0f23d..2e747782c 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -6,10 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZGcd.
+Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor
+ ZGcd ZLcm.
 
 (** This functor summarizes all known facts about Z. *)
 
 Module Type ZProp (Z:ZAxiomsSig) :=
  ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
- <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z <+ ZGcdProp Z.
+ <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z
+ <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index b2bf8703e..72137eccf 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -19,17 +19,14 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
     - [ZMake.Make BigN] provides the operations and basic specs w.r.t. ZArith
     - [ZTypeIsZAxioms] shows (mainly) that these operations implement
       the interface [ZAxioms]
-    - [ZPropSig] adds all generic properties derived from [ZAxioms]
-    - [ZDivPropFunct] provides generic properties of [div] and [mod]
-      ("Floor" variant)
+    - [ZProp] adds all generic properties derived from [ZAxioms]
     - [MinMax*Properties] provides properties of [min] and [max]
 
 *)
 
 
 Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
- ZMake.Make BigN <+ ZTypeIsZAxioms
- <+ !ZProp <+ !ZDivProp <+ HasEqBool2Dec
+ ZMake.Make BigN <+ ZTypeIsZAxioms <+ !ZProp <+ HasEqBool2Dec
  <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
 
 (** Notations about [BigZ] *)
@@ -67,6 +64,8 @@ Arguments Scope BigZ.log2 [bigZ_scope].
 Arguments Scope BigZ.sqrt [bigZ_scope].
 Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.quot [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.remainder [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.even [bigZ_scope].
 Arguments Scope BigZ.odd [bigZ_scope].
@@ -92,7 +91,9 @@ Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope.
 Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
 Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
-Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope.
+Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
+Infix "rem" := BigZ.remainder (at level 40, no associativity) : bigZ_scope.
+Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
 
 Local Open Scope bigZ_scope.
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index b341b3209..f4baf32bc 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith.
+Require Import ZArith Zquot.
 Require Import BigNumPrelude.
 Require Import NSig.
 Require Import ZSig.
@@ -453,6 +453,44 @@ Module Make (N:NType) <: ZType.
  intros q r q11 r1 H; injection H; auto.
  Qed.
 
+ Definition quot x y :=
+  match x, y with
+  | Pos nx, Pos ny => Pos (N.div nx ny)
+  | Pos nx, Neg ny => Neg (N.div nx ny)
+  | Neg nx, Pos ny => Neg (N.div nx ny)
+  | Neg nx, Neg ny => Pos (N.div nx ny)
+  end.
+
+ Definition remainder x y :=
+  if eq_bool y zero then x
+  else
+    match x, y with
+      | Pos nx, Pos ny => Pos (N.modulo nx ny)
+      | Pos nx, Neg ny => Pos (N.modulo nx ny)
+      | Neg nx, Pos ny => Neg (N.modulo nx ny)
+      | Neg nx, Neg ny => Neg (N.modulo nx ny)
+    end.
+
+ Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).
+ Proof.
+  intros [x|x] [y|y]; simpl; symmetry;
+   rewrite N.spec_div, ?Zquot_opp_r, ?Zquot_opp_l, ?Zopp_involutive;
+   rewrite Zquot_Zdiv_pos; trivial using N.spec_pos.
+ Qed.
+
+ Lemma spec_remainder : forall x y,
+   to_Z (remainder x y) = (to_Z x) rem (to_Z y).
+ Proof.
+  intros x y. unfold remainder. rewrite spec_eq_bool, spec_0.
+  assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
+  now rewrite Hy, Zrem_0_r.
+  destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
+   rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive;
+   try rewrite Z.eq_opp_l, Z.opp_0 in Hy;
+   rewrite Zrem_Zmod_pos; generalize (N.spec_pos x) (N.spec_pos y);
+   z_order.
+ Qed.
+
  Definition gcd x y :=
   match x, y with
   | Pos nx, Pos ny => Pos (N.gcd nx ny)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 01d36854b..f68aa0dbe 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,7 +10,7 @@
 
 
 Require Import ZAxioms ZProperties BinInt Zcompare Zorder ZArith_dec
- Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def.
+ Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def Zdiv_def.
 
 Local Open Scope Z_scope.
 
@@ -170,6 +170,27 @@ Definition gcd_nonneg := Zgcd_nonneg.
 Definition divide := Zdivide'.
 Definition gcd := Zgcd.
 
+(** Div / Mod / Quot / Rem *)
+
+Program Instance div_wd : Proper (eq==>eq==>eq) Zdiv.
+Program Instance mod_wd : Proper (eq==>eq==>eq) Zmod.
+Program Instance quot_wd : Proper (eq==>eq==>eq) Zquot.
+Program Instance rem_wd : Proper (eq==>eq==>eq) Zrem.
+
+Definition div_mod := Z_div_mod_eq_full.
+Definition mod_pos_bound := Zmod_pos_bound.
+Definition mod_neg_bound := Zmod_neg_bound.
+Definition mod_bound_pos := fun a b (_:0<=a) => Zmod_pos_bound a b.
+Definition div := Zdiv.
+Definition modulo := Zmod.
+
+Definition quot_rem := fun a b (_:b<>0) => Z_quot_rem_eq a b.
+Definition rem_bound_pos := Zrem_bound.
+Definition rem_opp_l := fun a b (_:b<>0) => Zrem_opp_l a b.
+Definition rem_opp_r := fun a b (_:b<>0) => Zrem_opp_r a b.
+Definition quot := Zquot.
+Definition remainder := Zrem.
+
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
 Definition eq := (@eq Z).
@@ -212,18 +233,3 @@ exact Zadd_opp_r.
 Qed.
 
 Add Ring ZR : Zring.*)
-
-
-
-(*
-Theorem eq_equiv_e : forall x y : Z, E x y <-> e x y.
-Proof.
-intros x y; unfold E, e, Zeq_bool; split; intro H.
-rewrite H; now rewrite Zcompare_refl.
-rewrite eq_true_unfold_pos in H.
-assert (H1 : (x ?= y) = Eq).
-case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H;
-[reflexivity | discriminate H | discriminate H].
-now apply Zcompare_Eq_eq.
-Qed.
-*)
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index b5c761a6f..c2a173e22 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -55,6 +55,8 @@ Module Type ZType.
  Parameter div_eucl : t -> t -> t * t.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
+ Parameter quot : t -> t -> t.
+ Parameter remainder : t -> t -> t.
  Parameter gcd : t -> t -> t.
  Parameter sgn : t -> t.
  Parameter abs : t -> t.
@@ -85,6 +87,8 @@ Module Type ZType.
    let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
+ Parameter spec_quot: forall x y, [quot x y] = [x] ÷ [y].
+ Parameter spec_remainder: forall x y, [remainder x y] = [x] rem [y].
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 999e7cd03..6a823a732 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,13 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith Nnat ZAxioms ZDivFloor ZSig.
-
-(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig]
-
-    It also provides [sgn], [abs], [div], [mod]
-*)
+Require Import ZArith Nnat ZAxioms ZSig.
 
+(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
 Module ZTypeIsZAxioms (Import Z : ZType').
 
@@ -20,7 +16,8 @@ Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd
+ spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot
+ spec_remainder
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -349,6 +346,36 @@ Proof.
 intros a b. zify. intros. apply Z_mod_neg; auto with zarith.
 Qed.
 
+Definition mod_bound_pos :
+ forall a b, 0<=a -> 0<b -> 0 <= modulo a b /\ modulo a b < b :=
+ fun a b _ H => mod_pos_bound a b H.
+
+(** Quot / Rem *)
+
+Program Instance quot_wd : Proper (eq==>eq==>eq) quot.
+Program Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+
+Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + (remainder a b).
+Proof.
+intros a b _. zify. apply Z_quot_rem_eq.
+Qed.
+
+Theorem rem_bound_pos :
+ forall a b, 0<=a -> 0<b -> 0 <= remainder a b /\ remainder a b < b.
+Proof.
+intros a b. zify. intros. now apply Zrem_bound.
+Qed.
+
+Theorem rem_opp_l : forall a b, ~b==0 -> remainder (-a) b == -(remainder a b).
+Proof.
+intros a b _. zify. apply Zrem_opp_l.
+Qed.
+
+Theorem rem_opp_r : forall a b, ~b==0 -> remainder a (-b) == remainder a b.
+Proof.
+intros a b _. zify. apply Zrem_opp_r.
+Qed.
+
 (** Gcd *)
 
 Definition divide n m := exists p, n*p == m.
@@ -384,5 +411,5 @@ Qed.
 End ZTypeIsZAxioms.
 
 Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
+ <: ZAxiomsSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
  := Z <+ ZTypeIsZAxioms.