BigN, BigZ, BigQ: presentation via unique module with both ops and props

 We use the <+ operation to regroup all known facts about BigN
 (resp BigZ, ...) in a unique module. This uses also the new ! feature
 for controling inlining. By the way, we also make sure that these
 new BigN and BigZ modules implements OrderedTypeFull and TotalOrder,
 and also contains facts about min and max (cf. GenericMinMax).

 Side effects:
 - In NSig and ZSig, specification of compare and eq_bool is now
   done with respect to Zcompare and Zeq_bool, as for other ops.
   The order <= and < are also defined via Zle and Zlt, instead
   of using compare. Min and max are axiomatized instead of being
   macros.
 - Some proofs rework in QMake
 - QOrderedType and Qminmax were in fact not compiled by make world

 Still todo: OrderedType + MinMax for BigQ, etc etc

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

4 files changed, 281 insertions, 442 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index fc94f693af..73cc5c21b9 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -13,13 +13,26 @@
 Require Export BigN.
 Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
-Module BigZ <: ZType := ZMake.Make BigN.
+(** * [BigZ] : arbitrary large efficient integers.
 
-(** Module [BigZ] implements [ZAxiomsSig] *)
+    The following [BigZ] module regroups both the operations and
+    all the abstract properties:
 
-Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
-Module Export BigZPropMod := ZPropFunct BigZAxiomsMod.
-Module Export BigZDivPropMod := ZDivPropFunct BigZAxiomsMod BigZPropMod.
+    - [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)
+    - [MinMax*Properties] provides properties of [min] and [max]
+
+*)
+
+
+Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
+ ZMake.Make BigN <+ ZTypeIsZAxioms
+ <+ !ZPropSig <+ !ZDivPropFunct <+ HasEqBool2Dec
+ <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
 
 (** Notations about [BigZ] *)
 
@@ -69,7 +82,7 @@ Infix "<=" := BigZ.le : bigZ_scope.
 Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
 Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
-Infix "mod" := modulo (at level 40, no associativity) : bigN_scope.
+Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope.
 
 Local Open Scope bigZ_scope.
 
@@ -102,35 +115,34 @@ intros p1 _ H1; case H1; auto.
 intros p1 H1; case H1; auto.
 Qed.
 
-Lemma sub_opp : forall x y : bigZ, x - y == x + (- y).
-Proof.
-red; intros; zsimpl; auto.
-Qed.
-
-Lemma add_opp : forall x : bigZ, x + (- x) == 0.
-Proof.
-red; intros; zsimpl; auto with zarith.
-Qed.
-
 (** [BigZ] is a ring *)
 
 Lemma BigZring :
  ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
 Proof.
 constructor.
-exact add_0_l.
-exact add_comm.
-exact add_assoc.
-exact mul_1_l.
-exact mul_comm.
-exact mul_assoc.
-exact mul_add_distr_r.
-exact sub_opp.
-exact add_opp.
+exact BigZ.add_0_l.
+exact BigZ.add_comm.
+exact BigZ.add_assoc.
+exact BigZ.mul_1_l.
+exact BigZ.mul_comm.
+exact BigZ.mul_assoc.
+exact BigZ.mul_add_distr_r.
+symmetry. apply BigZ.add_opp_r.
+exact BigZ.add_opp_diag_r.
 Qed.
 
 Add Ring BigZr : BigZring.
 
+(** [BigZ] benefits from an "order" tactic *)
+
+Ltac bigZ_order := BigZ.order.
+
+Section Test.
+Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
+Proof. bigZ_order. Qed.
+End Test.
+
 (** Todo: tactic translating from [BigZ] to [Z] + omega *)
 
 (** Todo: micromega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 0ab509650a..05c7ee32f3 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -49,6 +49,7 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_of_Z: forall x, to_Z (of_Z x) = x.
+ Proof.
  intros x; case x; unfold to_Z, of_Z, zero.
    exact N.spec_0.
    intros; rewrite N.spec_of_N; auto.
@@ -85,34 +86,23 @@ Module Make (N:NType) <: ZType.
   | Neg nx, Neg ny => N.compare ny nx
   end.
 
- Definition lt n m := compare n m = Lt.
- Definition le n m := compare n m <> Gt.
- Definition min n m := match compare n m with Gt => m | _ => n end.
- Definition max n m := match compare n m with Lt => m | _ => n end.
-
- Theorem spec_compare: forall x y,
-    match compare x y with
-      Eq => to_Z x = to_Z y
-    | Lt => to_Z x < to_Z y
-    | Gt => to_Z x > to_Z y
-    end.
-  unfold compare, to_Z; intros x y; case x; case y; clear x y;
-    intros x y; auto; generalize (N.spec_pos x) (N.spec_pos y).
-  generalize (N.spec_compare y x); case N.compare; auto with zarith.
-  generalize (N.spec_compare y N.zero); case N.compare;
-     try rewrite N.spec_0; auto with zarith.
-  generalize (N.spec_compare x N.zero); case N.compare;
-   rewrite N.spec_0; auto with zarith.
-  generalize (N.spec_compare x N.zero); case N.compare;
-   rewrite N.spec_0; auto with zarith.
-  generalize (N.spec_compare N.zero y); case N.compare;
-     try rewrite N.spec_0; auto with zarith.
-  generalize (N.spec_compare N.zero x); case N.compare;
-   rewrite N.spec_0; auto with zarith.
-  generalize (N.spec_compare N.zero x); case N.compare;
-   rewrite N.spec_0; auto with zarith.
-  generalize (N.spec_compare x y); case N.compare; auto with zarith.
-  Qed.
+ Theorem spec_compare :
+  forall x y, compare x y = Zcompare (to_Z x) (to_Z y).
+ Proof.
+ unfold compare, to_Z.
+ destruct x as [x|x], y as [y|y];
+ rewrite ?N.spec_compare, ?N.spec_0, <-?Zcompare_opp; auto;
+ assert (Hx:=N.spec_pos x); assert (Hy:=N.spec_pos y);
+ set (X:=N.to_Z x) in *; set (Y:=N.to_Z y) in *; clearbody X Y.
+ destruct (Zcompare_spec X 0) as [EQ|LT|GT].
+  rewrite EQ. rewrite <- Zopp_0 at 2. apply Zcompare_opp.
+  exfalso. omega.
+  symmetry. change (X > -Y). omega.
+ destruct (Zcompare_spec 0 X) as [EQ|LT|GT].
+  rewrite <- EQ. rewrite Zopp_0; auto.
+  symmetry. change (-X < Y). omega.
+  exfalso. omega.
+ Qed.
 
  Definition eq_bool x y :=
   match compare x y with
@@ -120,36 +110,27 @@ Module Make (N:NType) <: ZType.
   | _ => false
   end.
 
- Theorem spec_eq_bool: forall x y,
-    if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y.
- intros x y; unfold eq_bool;
-   generalize (spec_compare x y); case compare; auto with zarith.
+ Theorem spec_eq_bool:
+  forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y).
+ Proof.
+ unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity.
  Qed.
 
- Definition cmp_sign x y :=
-  match x, y with
-  | Pos nx, Neg ny =>
-    if N.eq_bool ny N.zero then Eq else Gt
-  | Neg nx, Pos ny =>
-    if N.eq_bool nx N.zero then Eq else Lt
-  | _, _ => Eq
-  end.
+ Definition lt n m := to_Z n < to_Z m.
+ Definition le n m := to_Z n <= to_Z m.
 
- Theorem spec_cmp_sign: forall x y,
-  match cmp_sign x y with
-  | Gt => 0 <= to_Z x /\ to_Z y < 0
-  | Lt => to_Z x <  0 /\ 0 <= to_Z y
-  | Eq => True
-  end.
-  Proof.
-  intros [x | x] [y | y]; unfold cmp_sign; auto.
-  generalize (N.spec_eq_bool y N.zero); case N.eq_bool; auto.
-  rewrite N.spec_0; unfold to_Z.
-  generalize (N.spec_pos x) (N.spec_pos y); auto with zarith.
-  generalize (N.spec_eq_bool x N.zero); case N.eq_bool; auto.
-  rewrite N.spec_0; unfold to_Z.
-  generalize (N.spec_pos x) (N.spec_pos y); auto with zarith.
-  Qed.
+ Definition min n m := match compare n m with Gt => m | _ => n end.
+ Definition max n m := match compare n m with Lt => m | _ => n end.
+
+ Theorem spec_min : forall n m, to_Z (min n m) = Zmin (to_Z n) (to_Z m).
+ Proof.
+ unfold min, Zmin. intros. rewrite spec_compare. destruct Zcompare; auto.
+ Qed.
+
+ Theorem spec_max : forall n m, to_Z (max n m) = Zmax (to_Z n) (to_Z m).
+ Proof.
+ unfold max, Zmax. intros. rewrite spec_compare. destruct Zcompare; auto.
+ Qed.
 
  Definition to_N x :=
   match x with
@@ -160,6 +141,7 @@ Module Make (N:NType) <: ZType.
  Definition abs x := Pos (to_N x).
 
  Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z x).
+ Proof.
  intros x; case x; clear x; intros x; assert (F:=N.spec_pos x).
     simpl; rewrite Zabs_eq; auto.
  simpl; rewrite Zabs_non_eq; simpl; auto with zarith.
@@ -172,6 +154,7 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x.
+ Proof.
  intros x; case x; simpl; auto with zarith.
  Qed.
 
@@ -186,10 +169,10 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
+ Proof.
  intros x; case x; clear x; intros x.
    exact (N.spec_succ x).
- simpl; generalize (N.spec_compare N.zero x); case N.compare;
-   rewrite N.spec_0; simpl.
+ simpl. rewrite N.spec_compare. case Zcompare_spec; rewrite ?N.spec_0; simpl.
   intros HH; rewrite <- HH; rewrite N.spec_1; ring.
   intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith.
  generalize (N.spec_pos x); auto with zarith.
@@ -214,17 +197,11 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_add: forall x y, to_Z (add x y) = to_Z x +  to_Z y.
- unfold add, to_Z; intros [x | x] [y | y].
-   exact (N.spec_add x y).
- unfold zero; generalize (N.spec_compare x y); case N.compare.
-   rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
- unfold zero; generalize (N.spec_compare x y); case N.compare.
-   rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
- intros; rewrite N.spec_add; auto with zarith.
+ Proof.
+ unfold add, to_Z; intros [x | x] [y | y];
+   try (rewrite N.spec_add; auto with zarith);
+ rewrite N.spec_compare; case Zcompare_spec;
+  unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *.
  Qed.
 
  Definition pred x :=
@@ -238,12 +215,12 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1.
- unfold pred, to_Z, minus_one; intros [x | x].
-   generalize (N.spec_compare N.zero x); case N.compare;
-     rewrite N.spec_0; try rewrite N.spec_1; auto with zarith.
-   intros H; rewrite N.spec_pred, Zmax_r; auto with zarith.
- generalize (N.spec_pos x); auto with zarith.
- rewrite N.spec_succ; ring.
+ Proof.
+ unfold pred, to_Z, minus_one; intros [x | x];
+   try (rewrite N.spec_succ; ring).
+ rewrite N.spec_compare; case Zcompare_spec;
+  rewrite ?N.spec_0, ?N.spec_1, ?N.spec_pred;
+  generalize (N.spec_pos x); omega with *.
  Qed.
 
  Definition sub x y :=
@@ -265,17 +242,11 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y.
- unfold sub, to_Z; intros [x | x] [y | y].
- unfold zero; generalize (N.spec_compare x y); case N.compare.
-   rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
- rewrite N.spec_add; auto with zarith.
- rewrite N.spec_add; auto with zarith.
- unfold zero; generalize (N.spec_compare x y); case N.compare.
-   rewrite N.spec_0; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
- intros; rewrite N.spec_sub, Zmax_r; auto with zarith.
+ Proof.
+ unfold sub, to_Z; intros [x | x] [y | y];
+  try (rewrite N.spec_add; auto with zarith);
+ rewrite N.spec_compare; case Zcompare_spec;
+  unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *.
  Qed.
 
  Definition mul x y :=
@@ -286,8 +257,8 @@ Module Make (N:NType) <: ZType.
   | Neg nx, Neg ny => Pos (N.mul nx ny)
   end.
 
-
  Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.
+ Proof.
  unfold mul, to_Z; intros [x | x] [y | y]; rewrite N.spec_mul; ring.
  Qed.
 
@@ -298,6 +269,7 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_square: forall x, to_Z (square x) = to_Z x *  to_Z x.
+ Proof.
  unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring.
  Qed.
 
@@ -313,6 +285,7 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
+ Proof.
  assert (F0: forall x, (-x)^2 = x^2).
    intros x; rewrite Zpower_2; ring.
  unfold power_pos, to_Z; intros [x | x] [p | p |];
@@ -335,9 +308,9 @@ Module Make (N:NType) <: ZType.
   | Neg nx => Neg N.zero
   end.
 
-
  Theorem spec_sqrt: forall x, 0 <= to_Z x ->
    to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
+ Proof.
  unfold to_Z, sqrt; intros [x | x] H.
    exact (N.spec_sqrt x).
  replace (N.to_Z x) with 0.
@@ -353,144 +326,74 @@ Module Make (N:NType) <: ZType.
     (Pos q, Pos r)
   | Pos nx, Neg ny =>
     let (q, r) := N.div_eucl nx ny in
-    match N.compare N.zero r with
-    | Eq => (Neg q, zero)
-    | _ => (Neg (N.succ q), Neg (N.sub ny r))
-    end
+    if N.eq_bool N.zero r
+    then (Neg q, zero)
+    else (Neg (N.succ q), Neg (N.sub ny r))
   | Neg nx, Pos ny =>
     let (q, r) := N.div_eucl nx ny in
-    match N.compare N.zero r with
-    | Eq => (Neg q, zero)
-    | _ => (Neg (N.succ q), Pos (N.sub ny r))
-    end
+    if N.eq_bool N.zero r
+    then (Neg q, zero)
+    else (Neg (N.succ q), Pos (N.sub ny r))
   | Neg nx, Neg ny =>
     let (q, r) := N.div_eucl nx ny in
     (Pos q, Neg r)
   end.
 
-
- Theorem spec_div_eucl_nz: forall x y,
-      to_Z y <> 0 ->
-      let (q,r) := div_eucl x y in
-      (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
- unfold div_eucl, to_Z; intros [x | x] [y | y] H.
- assert (H1: 0 < N.to_Z y).
-   generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
- assert (HH: 0 < N.to_Z y).
-   generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
- intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl;
-   case_eq (N.to_Z x); case_eq (N.to_Z y);
-     try (intros; apply False_ind; auto with zarith; fail).
- intros p He1 He2 _ _ H1; injection H1; intros H2 H3.
- generalize (N.spec_compare N.zero r); case N.compare;
-   unfold zero; rewrite N.spec_0; try rewrite H3; auto.
- rewrite H2; intros; apply False_ind; auto with zarith.
- rewrite H2; intros; apply False_ind; auto with zarith.
- intros p _ _ _ H1; discriminate H1.
- intros p He p1 He1 H1 _.
- generalize (N.spec_compare N.zero r); case N.compare.
- change (- Zpos p) with (Zneg p).
- unfold zero; lazy zeta.
- rewrite N.spec_0; intros H2; rewrite <- H2.
- intros H3; rewrite <- H3; auto.
- rewrite N.spec_0; intros H2.
- change (- Zpos p) with (Zneg p); lazy iota beta.
- intros H3; rewrite <- H3; auto.
- rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r.
- generalize H2; case (N.to_Z r).
- intros; apply False_ind; auto with zarith.
- intros p2 _; rewrite He; auto with zarith.
- change (Zneg p) with (- (Zpos p)); apply f_equal2 with (f := @pair Z Z); ring.
- intros p2 H4; discriminate H4.
- assert (N.to_Z r = (Zpos p1 mod (Zpos p))).
-   unfold Zmod, Zdiv_eucl; rewrite <- H3; auto.
- case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith.
- rewrite N.spec_0; intros H2; generalize (N.spec_pos r);
-   intros; apply False_ind; auto with zarith.
- assert (HH: 0 < N.to_Z y).
-   generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
- intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl;
-   case_eq (N.to_Z x); case_eq (N.to_Z y);
-     try (intros; apply False_ind; auto with zarith; fail).
- intros p He1 He2 _ _ H1; injection H1; intros H2 H3.
- generalize (N.spec_compare N.zero r); case N.compare;
-   unfold zero; rewrite N.spec_0; try rewrite H3; auto.
- rewrite H2; intros; apply False_ind; auto with zarith.
- rewrite H2; intros; apply False_ind; auto with zarith.
- intros p _ _ _ H1; discriminate H1.
- intros p He p1 He1 H1 _.
- generalize (N.spec_compare N.zero r); case N.compare.
- change (- Zpos p1) with (Zneg p1).
- unfold zero; lazy zeta.
- rewrite N.spec_0; intros H2; rewrite <- H2.
- intros H3; rewrite <- H3; auto.
- rewrite N.spec_0; intros H2.
- change (- Zpos p1) with (Zneg p1); lazy iota beta.
- intros H3; rewrite <- H3; auto.
- rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r.
- generalize H2; case (N.to_Z r).
- intros; apply False_ind; auto with zarith.
- intros p2 _; rewrite He; auto with zarith.
- intros p2 H4; discriminate H4.
- assert (N.to_Z r = (Zpos p1 mod (Zpos p))).
-   unfold Zmod, Zdiv_eucl; rewrite <- H3; auto.
- case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith.
- rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith.
- assert (H1: 0 < N.to_Z y).
-   generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
- intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl;
-   case_eq (N.to_Z x); case_eq (N.to_Z y);
-     try (intros; apply False_ind; auto with zarith; fail).
- change (-0) with 0; lazy iota beta; auto.
- intros p _ _ _ _ H2; injection H2.
- intros H3 H4; rewrite H3; rewrite H4; auto.
- intros p _ _ _ H2; discriminate H2.
- intros p He p1 He1 _ _  H2.
- change (- Zpos p1) with (Zneg p1); lazy iota beta.
- change (- Zpos p) with (Zneg p); lazy iota beta.
- rewrite <- H2; auto.
- Qed.
-
- Lemma Zdiv_eucl_0 : forall a, Zdiv_eucl a 0 = (0,0).
- Proof. destruct a; auto. Qed.
+ Ltac break_nonneg x px EQx :=
+  let H := fresh "H" in
+  assert (H:=N.spec_pos x);
+  destruct (N.to_Z x) as [|px|px]_eqn:EQx;
+   [clear H|clear H|elim H; reflexivity].
 
  Theorem spec_div_eucl: forall x y,
-      let (q,r) := div_eucl x y in
-      (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
+   let (q,r) := div_eucl x y in
+   (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
  Proof.
- intros. destruct (Z_eq_dec (to_Z y) 0) as [EQ|NEQ];
-  [|apply spec_div_eucl_nz; auto].
- unfold div_eucl.
- destruct x; destruct y; simpl in *.
- generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
- generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
- assert (EQ' : N.to_Z t1 = 0) by auto with zarith.
- rewrite EQ'. simpl. rewrite Zdiv_eucl_0. injection 1; intros.
- generalize (N.spec_compare N.zero t3); destruct N.compare.
- simpl. intros. f_equal; auto with zarith.
- rewrite N.spec_0; intro; exfalso; auto with zarith.
- rewrite N.spec_0; intro; exfalso; auto with zarith.
- generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
- assert (EQ' : N.to_Z t1 = 0) by auto with zarith.
- rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros.
- generalize (N.spec_compare N.zero t3); destruct N.compare.
- simpl. intros. f_equal; auto with zarith.
- rewrite N.spec_0; intro; exfalso; auto with zarith.
- rewrite N.spec_0; intro; exfalso; auto with zarith.
- generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
- assert (EQ' : N.to_Z t1 = 0) by auto with zarith.
- rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros.
- f_equal; auto with zarith.
+ unfold div_eucl, to_Z. intros [x | x] [y | y].
+ (* Pos Pos *)
+ generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y); auto.
+ (* Pos Neg *)
+ generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
+ break_nonneg x px EQx; break_nonneg y py EQy;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+      simpl; rewrite Hq, N.spec_0; auto).
+ change (- Zpos py) with (Zneg py).
+ assert (GT : Zpos py > 0) by (compute; auto).
+ generalize (Z_div_mod (Zpos px) (Zpos py) GT).
+ unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
+ intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ break_nonneg r pr EQr.
+ subst; simpl. rewrite N.spec_0; auto.
+ subst. lazy iota beta delta [Zeq_bool Zcompare].
+ rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
+ (* Neg Pos *)
+ generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
+ break_nonneg x px EQx; break_nonneg y py EQy;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+      simpl; rewrite Hq, N.spec_0; auto).
+ change (- Zpos px) with (Zneg px).
+ assert (GT : Zpos py > 0) by (compute; auto).
+ generalize (Z_div_mod (Zpos px) (Zpos py) GT).
+ unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
+ intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ break_nonneg r pr EQr.
+ subst; simpl. rewrite N.spec_0; auto.
+ subst. lazy iota beta delta [Zeq_bool Zcompare].
+ rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
+ (* Neg Neg *)
+ generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
+ break_nonneg x px EQx; break_nonneg y py EQy;
+ try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto).
+ simpl. intros <-; auto.
  Qed.
 
  Definition div x y := fst (div_eucl x y).
 
  Definition spec_div: forall x y,
      to_Z (div x y) = to_Z x / to_Z y.
+ Proof.
  intros x y; generalize (spec_div_eucl x y); unfold div, Zdiv.
  case div_eucl; case Zdiv_eucl; simpl; auto.
  intros q r q11 r1 H; injection H; auto.
@@ -500,6 +403,7 @@ Module Make (N:NType) <: ZType.
 
  Theorem spec_modulo:
    forall x y, to_Z (modulo x y) = to_Z x mod to_Z y.
+ Proof.
  intros x y; generalize (spec_div_eucl x y); unfold modulo, Zmod.
  case div_eucl; case Zdiv_eucl; simpl; auto.
  intros q r q11 r1 H; injection H; auto.
@@ -514,6 +418,7 @@ Module Make (N:NType) <: ZType.
   end.
 
  Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
+ Proof.
  unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd;
   auto; case N.to_Z; simpl; auto with zarith;
   try rewrite Zabs_Zopp; auto;
@@ -529,8 +434,7 @@ Module Make (N:NType) <: ZType.
 
  Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x).
  Proof.
- intros. unfold sgn. generalize (spec_compare zero x).
- destruct compare.
+ intros. unfold sgn. rewrite spec_compare. case Zcompare_spec.
  rewrite spec_0. intros <-; auto.
  rewrite spec_0, spec_1. symmetry. rewrite Zsgn_pos; auto.
  rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index a7c5473aa3..a9945e848c 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -25,100 +25,75 @@ Module Type ZType.
  Parameter t : Type.
 
  Parameter to_Z : t -> Z.
- Notation "[ x ]" := (to_Z x).
+ Local Notation "[ x ]" := (to_Z x).
 
- Definition eq x y := ([x] = [y]).
+ Definition eq x y := [x] = [y].
+ Definition lt x y := [x] < [y].
+ Definition le x y := [x] <= [y].
 
  Parameter of_Z : Z -> t.
  Parameter spec_of_Z: forall x, to_Z (of_Z x) = x.
 
+ Parameter compare : t -> t -> comparison.
+ Parameter eq_bool : t -> t -> bool.
+ Parameter min : t -> t -> t.
+ Parameter max : t -> t -> t.
  Parameter zero : t.
  Parameter one : t.
  Parameter minus_one : t.
+ Parameter succ : t -> t.
+ Parameter add  : t -> t -> t.
+ Parameter pred : t -> t.
+ Parameter sub : t -> t -> t.
+ Parameter opp : t -> t.
+ Parameter mul : t -> t -> t.
+ Parameter square : t -> t.
+ Parameter power_pos : t -> positive -> t.
+ Parameter sqrt : t -> t.
+ Parameter div_eucl : t -> t -> t * t.
+ Parameter div : t -> t -> t.
+ Parameter modulo : t -> t -> t.
+ Parameter gcd : t -> t -> t.
+ Parameter sgn : t -> t.
+ Parameter abs : t -> t.
 
+ Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
+ Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
+ Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
+ Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
  Parameter spec_m1: [minus_one] = -1.
-
- Parameter compare : t -> t -> comparison.
-
- Parameter spec_compare: forall x y,
-   match compare x y with
-     | Eq => [x] = [y]
-     | Lt => [x] < [y]
-     | Gt => [x] > [y]
-   end.
-
- Definition lt n m := compare n m = Lt.
- Definition le n m := compare n m <> Gt.
- Definition min n m := match compare n m with Gt => m | _ => n end.
- Definition max n m := match compare n m with Lt => m | _ => n end.
-
- Parameter eq_bool : t -> t -> bool.
-
- Parameter spec_eq_bool: forall x y,
-    if eq_bool x y then [x] = [y] else [x] <> [y].
-
- Parameter succ : t -> t.
-
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
-
- Parameter add  : t -> t -> t.
-
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
-
- Parameter pred : t -> t.
-
  Parameter spec_pred: forall x, [pred x] = [x] - 1.
-
- Parameter sub : t -> t -> t.
-
  Parameter spec_sub: forall x y, [sub x y] = [x] - [y].
-
- Parameter opp : t -> t.
-
  Parameter spec_opp: forall x, [opp x] = - [x].
-
- Parameter mul : t -> t -> t.
-
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
-
- Parameter square : t -> t.
-
  Parameter spec_square: forall x, [square x] = [x] *  [x].
-
- Parameter power_pos : t -> positive -> t.
-
  Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
-
- Parameter sqrt : t -> t.
-
  Parameter spec_sqrt: forall x, 0 <= [x] ->
    [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
-
- Parameter div_eucl : t -> t -> t * t.
-
  Parameter spec_div_eucl: forall x y,
    let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
-
- Parameter div : t -> t -> t.
-
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
-
- Parameter modulo : t -> t -> t.
-
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
-
- Parameter gcd : t -> t -> t.
-
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b).
-
- Parameter sgn : t -> t.
-
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
-
- Parameter abs : t -> t.
-
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
 
 End ZType.
+
+Module Type ZType_Notation (Import Z:ZType).
+ Notation "[ x ]" := (to_Z x).
+ Infix "=="  := eq (at level 70).
+ Notation "0" := zero.
+ Infix "+" := add.
+ Infix "-" := sub.
+ Infix "*" := mul.
+ Notation "- x" := (opp x).
+ Infix "<=" := le.
+ Infix "<" := lt.
+End ZType_Notation.
+
+Module Type ZType' := ZType <+ ZType_Notation.
\ No newline at end of file
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index a94e1a318f..3d53707eb8 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -16,71 +16,64 @@ Require Import ZArith ZAxioms ZDivFloor ZSig.
 *)
 
 
-Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig <: ZDivSig.
-
-Local Notation "[ x ]" := (Z.to_Z x).
-Local Infix "=="  := Z.eq (at level 70).
-Local Notation "0" := Z.zero.
-Local Infix "+" := Z.add.
-Local Infix "-" := Z.sub.
-Local Infix "*" := Z.mul.
-Local Notation "- x" := (Z.opp x).
-Local Infix "<=" := Z.le.
-Local Infix "<" := Z.lt.
+Module ZTypeIsZAxioms (Import Z : ZType').
 
 Hint Rewrite
- Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
- Z.spec_mul Z.spec_opp Z.spec_of_Z Z.spec_div Z.spec_modulo: zspec.
+ spec_0 spec_1 spec_add spec_sub spec_pred spec_succ
+ spec_mul spec_opp spec_of_Z spec_div spec_modulo
+ spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
+ : zsimpl.
 
-Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec.
+Ltac zsimpl := autorewrite with zsimpl.
 Ltac zcongruence := repeat red; intros; zsimpl; congruence.
+Ltac zify := unfold eq, lt, le in *; zsimpl.
 
-Instance eq_equiv : Equivalence Z.eq.
-Proof. unfold Z.eq. firstorder. Qed.
+Instance eq_equiv : Equivalence eq.
+Proof. unfold eq. firstorder. Qed.
 
 Local Obligation Tactic := zcongruence.
 
-Program Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ.
-Program Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred.
-Program Instance add_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add.
-Program Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub.
-Program Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul.
+Program Instance succ_wd : Proper (eq ==> eq) succ.
+Program Instance pred_wd : Proper (eq ==> eq) pred.
+Program Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
 
-Theorem pred_succ : forall n, Z.pred (Z.succ n) == n.
+Theorem pred_succ : forall n, pred (succ n) == n.
 Proof.
-intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
 Section Induction.
 
 Variable A : Z.t -> Prop.
-Hypothesis A_wd : Proper (Z.eq==>iff) A.
+Hypothesis A_wd : Proper (eq==>iff) A.
 Hypothesis A0 : A 0.
-Hypothesis AS : forall n, A n <-> A (Z.succ n).
+Hypothesis AS : forall n, A n <-> A (succ n).
 
-Let B (z : Z) := A (Z.of_Z z).
+Let B (z : Z) := A (of_Z z).
 
 Lemma B0 : B 0.
 Proof.
 unfold B; simpl.
 rewrite <- (A_wd 0); auto.
-zsimpl; auto.
+zify. auto.
 Qed.
 
 Lemma BS : forall z : Z, B z -> B (z + 1).
 Proof.
 intros z H.
 unfold B in *. apply -> AS in H.
-setoid_replace (Z.of_Z (z + 1)) with (Z.succ (Z.of_Z z)); auto.
-zsimpl; auto.
+setoid_replace (of_Z (z + 1)) with (succ (of_Z z)); auto.
+zify. auto.
 Qed.
 
 Lemma BP : forall z : Z, B z -> B (z - 1).
 Proof.
 intros z H.
 unfold B in *. rewrite AS.
-setoid_replace (Z.succ (Z.of_Z (z - 1))) with (Z.of_Z z); auto.
-zsimpl; auto with zarith.
+setoid_replace (succ (of_Z (z - 1))) with (of_Z z); auto.
+zify. auto with zarith.
 Qed.
 
 Lemma B_holds : forall z : Z, B z.
@@ -99,213 +92,168 @@ Qed.
 
 Theorem bi_induction : forall n, A n.
 Proof.
-intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)).
+intro n. setoid_replace n with (of_Z (to_Z n)).
 apply B_holds.
-zsimpl; auto.
+zify. auto.
 Qed.
 
 End Induction.
 
 Theorem add_0_l : forall n, 0 + n == n.
 Proof.
-intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem add_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
+Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m).
 Proof.
-intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
 Theorem sub_0_r : forall n, n - 0 == n.
 Proof.
-intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem sub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
+Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m).
 Proof.
-intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
 Theorem mul_0_l : forall n, 0 * n == 0.
 Proof.
-intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
+Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m.
 Proof.
-intros; zsimpl; ring.
+intros. zify. ring.
 Qed.
 
 (** Order *)
 
-Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z.
+Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 Proof.
- intros; generalize (Z.spec_compare x y).
- destruct (Z.compare x y); auto.
- intros H; rewrite H; symmetry; apply Zcompare_refl.
+ intros. zify. destruct (Zcompare_spec [x] [y]); auto.
 Qed.
 
-Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
-Proof.
- intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition.
-Qed.
-
-Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
-Proof.
- intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition.
-Qed.
-
-Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y].
-Proof.
- intros; unfold Z.min, Zmin.
- rewrite spec_compare_alt; destruct Zcompare; auto.
-Qed.
+Definition eqb := eq_bool.
 
-Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y].
+Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
 Proof.
- intros; unfold Z.max, Zmax.
- rewrite spec_compare_alt; destruct Zcompare; auto.
+ intros. zify. symmetry. apply Zeq_is_eq_bool.
 Qed.
 
-Instance compare_wd : Proper (Z.eq ==> Z.eq ==> eq) Z.compare.
+Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
-intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
 Qed.
 
-Instance lt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
 Proof.
-intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
 Qed.
 
 Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
 Proof.
-intros.
-unfold Z.eq; rewrite spec_lt, spec_le; omega.
+intros. zify. omega.
 Qed.
 
 Theorem lt_irrefl : forall n, ~ n < n.
 Proof.
-intros; rewrite spec_lt; auto with zarith.
+intros. zify. omega.
 Qed.
 
-Theorem lt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.
+Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
 Proof.
-intros; rewrite spec_lt, spec_le, Z.spec_succ; omega.
+intros. zify. omega.
 Qed.
 
-Theorem min_l : forall n m, n <= m -> Z.min n m == n.
+Theorem min_l : forall n m, n <= m -> min n m == n.
 Proof.
-intros n m; unfold Z.eq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
+intros n m. zify. omega with *.
 Qed.
 
-Theorem min_r : forall n m, m <= n -> Z.min n m == m.
+Theorem min_r : forall n m, m <= n -> min n m == m.
 Proof.
-intros n m; unfold Z.eq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
+intros n m. zify. omega with *.
 Qed.
 
-Theorem max_l : forall n m, m <= n -> Z.max n m == n.
+Theorem max_l : forall n m, m <= n -> max n m == n.
 Proof.
-intros n m; unfold Z.eq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
+intros n m. zify. omega with *.
 Qed.
 
-Theorem max_r : forall n m, n <= m -> Z.max n m == m.
+Theorem max_r : forall n m, n <= m -> max n m == m.
 Proof.
-intros n m; unfold Z.eq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
+intros n m. zify. omega with *.
 Qed.
 
 (** Part specific to integers, not natural numbers *)
 
-Program Instance opp_wd : Proper (Z.eq ==> Z.eq) Z.opp.
+Program Instance opp_wd : Proper (eq ==> eq) opp.
 
-Theorem succ_pred : forall n, Z.succ (Z.pred n) == n.
+Theorem succ_pred : forall n, succ (pred n) == n.
 Proof.
-red; intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
 Theorem opp_0 : - 0 == 0.
 Proof.
-red; intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem opp_succ : forall n, - (Z.succ n) == Z.pred (- n).
+Theorem opp_succ : forall n, - (succ n) == pred (- n).
 Proof.
-intros; zsimpl; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem abs_eq : forall n, 0 <= n -> Z.abs n == n.
+Theorem abs_eq : forall n, 0 <= n -> abs n == n.
 Proof.
-intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs. apply Zabs_eq.
+intros n. zify. omega with *.
 Qed.
 
-Theorem abs_neq : forall n, n <= 0 -> Z.abs n == -n.
+Theorem abs_neq : forall n, n <= 0 -> abs n == -n.
 Proof.
-intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs, Z.spec_opp.
- apply Zabs_non_eq.
+intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_null : forall n, n==0 -> Z.sgn n == 0.
+Theorem sgn_null : forall n, n==0 -> sgn n == 0.
 Proof.
-intros n. unfold Z.eq. rewrite Z.spec_sgn, Z.spec_0. rewrite Zsgn_null; auto.
+intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_pos : forall n, 0<n -> Z.sgn n == Z.succ 0.
+Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0.
 Proof.
-intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_pos; auto.
+intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_neg : forall n, n<0 -> Z.sgn n == Z.opp (Z.succ 0).
+Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0).
 Proof.
-intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_neg; auto.
+intros n. zify. omega with *.
 Qed.
 
-Program Instance div_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.div.
-Program Instance mod_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.modulo.
+Program Instance div_wd : Proper (eq==>eq==>eq) div.
+Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
-Theorem div_mod : forall a b, ~b==0 -> a == b*(Z.div a b) + (Z.modulo a b).
+Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b).
 Proof.
-intros a b. unfold Z.eq; zsimpl. intros.
-apply Z_div_mod_eq_full; auto.
+intros a b. zify. intros. apply Z_div_mod_eq_full; auto.
 Qed.
 
 Theorem mod_pos_bound :
- forall a b, 0 < b -> 0 <= Z.modulo a b /\ Z.modulo a b < b.
+ forall a b, 0 < b -> 0 <= modulo a b /\ modulo a b < b.
 Proof.
-intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros.
-rewrite Z.spec_modulo; auto with zarith.
-apply Z_mod_lt; auto with zarith.
+intros a b. zify. intros. apply Z_mod_lt; auto with zarith.
 Qed.
 
 Theorem mod_neg_bound :
- forall a b, b < 0 -> b < Z.modulo a b /\ Z.modulo a b <= 0.
-Proof.
-intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros.
-rewrite Z.spec_modulo; auto with zarith.
-apply Z_mod_neg; auto with zarith.
-Qed.
-
-(** Aliases *)
-
-Definition t := Z.t.
-Definition eq := Z.eq.
-Definition zero := Z.zero.
-Definition succ := Z.succ.
-Definition pred := Z.pred.
-Definition add := Z.add.
-Definition sub := Z.sub.
-Definition mul := Z.mul.
-Definition opp := Z.opp.
-Definition lt := Z.lt.
-Definition le := Z.le.
-Definition min := Z.min.
-Definition max := Z.max.
-Definition abs := Z.abs.
-Definition sgn := Z.sgn.
-Definition div := Z.div.
-Definition modulo := Z.modulo.
-
-End ZSig_ZAxioms.
+ forall a b, b < 0 -> b < modulo a b /\ modulo a b <= 0.
+Proof.
+intros a b. zify. intros. apply Z_mod_neg; auto with zarith.
+Qed.
+
+End ZTypeIsZAxioms.
+
+Module ZType_ZAxioms (Z : ZType)
+ <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z
+ := Z <+ ZTypeIsZAxioms.