2 files changed, 39 insertions, 8 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index b5c761a6f2..c2a173e22a 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 999e7cd03e..6a823a7324 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.