Enhance the BigN and BigZ infrastructure:

 * Isolate and put forward the interfaces NSig and ZSig that describe
   what should contain structures of natural numbers and integers (specs 
   are done by translation to ZArith).

 * Functors NSigNAxioms and ZSigZAxioms proving that these NSig and 
   ZSig implements the fully-abstract NAxioms and ZAxioms module types.
   
 * BigN and BigZ now contains more notations, plus an export of all 
   abstract results proved by Evgeny instantiated thanks to NSigNAxioms
   and ZSigZAxioms. In addition, BigN and BigZ are declared as 
   (semi/full)-rings.

 * as a consequence, some incompatibities have to be fixed in BigQ: 
   - take care of some name masking (via Import, Open Scope ...)
   - some additionnal constants like BigN.lt to deal with



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

4 files changed, 519 insertions, 118 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 934fbc4280..d2f9b0a024 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -11,50 +11,99 @@
 (*i $Id$ i*)
 
 Require Export BigN.
+Require Import ZTimesOrder.
+Require Import ZSig.
+Require Import ZSigZAxioms.
 Require Import ZMake.
 
+Module BigZ <: ZType := ZMake.Make BigN.
 
-Module BigZ := Make BigN.
+(** Module [BigZ] implements [ZAxiomsSig] *)
 
+Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
+Module Export BigZTimesOrderPropMod := ZTimesOrderPropFunct BigZAxiomsMod.
 
-Definition bigZ := BigZ.t.
+(** Notations about [BigZ] *)
+
+Notation bigZ := BigZ.t.
 
 Delimit Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
 
-Notation " i + j " := (BigZ.add i j) : bigZ_scope.
-Notation " i - j " := (BigZ.sub i j) : bigZ_scope.
-Notation " i * j " := (BigZ.mul i j) : bigZ_scope.
-Notation " i / j " := (BigZ.div i j) : bigZ_scope.
-Notation " i ?= j " := (BigZ.compare i j) : bigZ_scope.
-
-
- Theorem spec_to_Z: 
-  forall n, BigN.to_Z (BigZ.to_N n) = 
-            (Zsgn (BigZ.to_Z n) * BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_N n: 
-  (BigZ.to_Z n = 
-    Zsgn (BigZ.to_Z n) * (BigN.to_Z (BigZ.to_N n)))%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
-
- Theorem spec_to_Z_pos: 
-  forall n, (0 <= BigZ.to_Z n ->
-              BigN.to_Z (BigZ.to_N n) = BigZ.to_Z n)%Z.
- intros n; case n; simpl; intros p; 
-     generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
- intros p1 _  H1; case H1; auto.
- intros p1 H1; case H1; auto.
- Qed.
+Notation Local "0" := BigZ.zero : bigZ_scope.
+Infix "+" := BigZ.add : bigZ_scope.
+Infix "-" := BigZ.sub : bigZ_scope.
+Notation "- x" := (BigZ.opp x) : bigZ_scope.
+Infix "*" := BigZ.mul : bigZ_scope.
+Infix "/" := BigZ.div : bigZ_scope.
+Infix "?=" := BigZ.compare : bigZ_scope.
+Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
+Infix "<" := BigZ.lt : bigZ_scope.
+Infix "<=" := BigZ.le : bigZ_scope.
+Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
+
+Open Scope bigZ_scope.
+
+(** Some additional results about [BigZ] *)
+
+Theorem spec_to_Z: forall n:bigZ, 
+  BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Theorem spec_to_N n: 
+ ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+intros p1 H1; case H1; auto.
+intros p1 H1; case H1; auto.
+Qed.
+
+Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
+  BigN.to_Z (BigZ.to_N n) = [n].
+Proof.
+intros n; case n; simpl; intros p; 
+  generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
+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 plus_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 Zplus_0_l.
+exact Zplus_comm.
+exact Zplus_assoc.
+exact Ztimes_1_l.
+exact Ztimes_comm.
+exact Ztimes_assoc.
+exact Ztimes_plus_distr_r.
+exact sub_opp.
+exact plus_opp.
+Qed.
+
+Add Ring BigZr : BigZring.
+
+(** 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 83171388d9..cbf6f701f2 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -12,94 +12,18 @@
 
 Require Import ZArith.
 Require Import BigNumPrelude.
+Require Import NSig.
+Require Import ZSig.
 
 Open Scope Z_scope.
 
-Module Type NType.
-
- Parameter t : Type.
- 
- Parameter zero : t.
- Parameter one : t.
-
- Parameter of_N : N -> t.
- Parameter to_Z : t -> Z.
- Parameter spec_pos: forall x, 0 <= to_Z x.
- Parameter spec_0: to_Z zero = 0.
- Parameter spec_1: to_Z one = 1.
- Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x.
-
- Parameter compare : t -> t -> comparison.
-
- Parameter 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.
-
- Parameter eq_bool : t -> t -> bool.
-
- Parameter 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.
- 
- Parameter succ : t -> t.
-
- Parameter spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
-
- Parameter add  : t -> t -> t.
-
- Parameter spec_add: forall x y, to_Z (add x y) = to_Z x +  to_Z y.
-
- Parameter pred : t -> t.
-
- Parameter spec_pred: forall x, 0 < to_Z x -> to_Z (pred x) = to_Z x - 1.
-
- Parameter sub  : t -> t -> t.
-
- Parameter spec_sub: forall x y, to_Z y <= to_Z x ->
-   to_Z (sub x y) = to_Z x - to_Z y.
-
- Parameter mul       : t -> t -> t.
-
- Parameter spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.
-
- Parameter square    : t -> t.
-
- Parameter spec_square: forall x, to_Z (square x) = to_Z x *  to_Z x.
-
- Parameter power_pos : t -> positive -> t.
-
- Parameter spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
-
- Parameter sqrt      : t -> t.
-
- Parameter spec_sqrt: forall x, to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
-
- Parameter div_eucl : t -> t -> t * t.
-
- Parameter spec_div_eucl: forall x y,
-      0 < 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)).
+(** * ZMake 
  
- Parameter div      : t -> t -> t.
-
- Parameter spec_div: forall x y,
-      0 < to_Z y -> to_Z (div x y) = to_Z x / to_Z y.
-
- Parameter modulo   : t -> t -> t.
-
- Parameter spec_modulo:
-   forall x y, 0 < to_Z y -> to_Z (modulo x y) = to_Z x mod to_Z y.
-
- Parameter gcd      : t -> t -> t.
-
- Parameter spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
-
-
-End NType.
+  A generic transformation from a structure of natural numbers 
+  [NSig.NType] to a structure of integers [ZSig.ZType].
+*)
 
-Module Make (N:NType).
+Module Make (N:NType) <: ZType.
  
  Inductive t_ := 
   | Pos : N.t -> t_
@@ -131,6 +55,7 @@ Module Make (N:NType).
    intros; rewrite N.spec_of_N; auto.
  Qed.
 
+ Definition eq x y := (to_Z x = to_Z y).
 
  Theorem spec_0: to_Z zero = 0.
  exact N.spec_0.
@@ -160,6 +85,10 @@ Module Make (N:NType).
   | 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
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
new file mode 100644
index 0000000000..4e45939831
--- /dev/null
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -0,0 +1,117 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith Znumtheory.
+
+Open Scope Z_scope.
+
+(** * ZSig *)
+
+(** Interface of a rich structure about integers.
+    Specifications are written via translation to Z.
+*)
+
+Module Type ZType.
+
+ Parameter t : Type.
+
+ Parameter to_Z : t -> Z.
+ Notation "[ x ]" := (to_Z x).
+
+ Definition eq x y := ([x] = [y]).
+
+ Parameter of_Z : Z -> t.
+ Parameter spec_of_Z: forall x, to_Z (of_Z x) = x.
+
+ Parameter zero : t.
+ Parameter one : t.
+ Parameter minus_one : t.
+
+ 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, [y] <> 0 ->
+   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, [y] <> 0 -> [div x y] = [x] / [y].
+
+ Parameter modulo : t -> t -> t.
+
+ Parameter spec_modulo: forall x y, [y] <> 0 -> 
+   [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).
+
+End ZType.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
new file mode 100644
index 0000000000..3d9d3d1901
--- /dev/null
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -0,0 +1,306 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import ZArith.
+Require Import ZAxioms.
+Require Import ZSig.
+
+(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
+
+Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
+
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.t.
+Open Local Scope IntScope.
+Notation "[ x ]" := (Z.to_Z x) : IntScope.
+Infix "=="  := Z.eq (at level 70) : IntScope.
+Notation "0" := Z.zero : IntScope.
+Infix "+" := Z.add : IntScope.
+Infix "-" := Z.sub : IntScope.
+Infix "*" := Z.mul : IntScope.
+Notation "- x" := (Z.opp x) : IntScope.
+
+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 : Zspec.
+
+Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec.
+
+Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
+Module Export NZAxiomsMod <: NZAxiomsSig.
+
+Definition NZ := Z.t.
+Definition NZeq := Z.eq.
+Definition NZ0 := Z.zero.
+Definition NZsucc := Z.succ.
+Definition NZpred := Z.pred.
+Definition NZplus := Z.add.
+Definition NZminus := Z.sub.
+Definition NZtimes := Z.mul.
+
+Theorem NZeq_equiv : equiv Z.t Z.eq.
+Proof.
+repeat split; repeat red; intros; auto; congruence.
+Qed.
+
+Add Relation Z.t Z.eq
+ reflexivity proved by (proj1 NZeq_equiv)
+ symmetry proved by (proj2 (proj2 NZeq_equiv))
+ transitivity proved by (proj1 (proj2 NZeq_equiv))
+ as NZeq_rel.
+
+Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZplus with signature Z.eq ==> Z.eq ==> Z.eq as NZplus_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Add Morphism NZtimes with signature Z.eq ==> Z.eq ==> Z.eq as NZtimes_wd.
+Proof.
+intros; zsimpl; f_equal; assumption.
+Qed.
+
+Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Section Induction.
+
+Variable A : Z.t -> Prop.
+Hypothesis A_wd : predicate_wd Z.eq A.
+Hypothesis A0 : A 0.
+Hypothesis AS : forall n, A n <-> A (Z.succ n). 
+
+Add Morphism A with signature Z.eq ==> iff as A_morph.
+Proof. apply A_wd. Qed.
+
+Let B (z : Z) := A (Z.of_Z z).
+
+Lemma B0 : B 0.
+Proof.
+unfold B; simpl.
+rewrite <- (A_wd 0); auto.
+zsimpl; 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.
+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.
+Qed.
+
+Lemma B_holds : forall z : Z, B z.
+Proof.
+intros; destruct (Z_lt_le_dec 0 z).
+apply natlike_ind; auto with zarith.
+apply B0.
+intros; apply BS; auto.
+replace z with (-(-z))%Z in * by (auto with zarith).
+remember (-z)%Z as z'.
+pattern z'; apply natlike_ind.
+apply B0.
+intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto.
+subst z'; auto with zarith.
+Qed.
+
+Theorem NZinduction : forall n, A n.
+Proof.
+intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)).
+apply B_holds.
+zsimpl; auto.
+Qed.
+
+End Induction.
+
+Theorem NZplus_0_l : forall n, 0 + n == n.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZplus_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZminus_0_r : forall n, n - 0 == n.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZtimes_0_l : forall n, 0 * n == 0.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem NZtimes_succ_l : forall n m, (Z.succ n) * m == n * m + m.
+Proof.
+intros; zsimpl; ring.
+Qed.
+
+End NZAxiomsMod.
+
+Definition NZlt := Z.lt.
+Definition NZle := Z.le.
+Definition NZmin := Z.min.
+Definition NZmax := Z.max.
+
+Infix "<=" := Z.le : IntScope.
+Infix "<" := Z.lt : IntScope.
+
+Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z.
+Proof.
+ intros; generalize (Z.spec_compare x y).
+ destruct (Z.compare x y); auto.
+ intros H; rewrite H; symmetry; apply Zcompare_refl.
+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.
+
+Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y].
+Proof.
+ intros; unfold Z.max, Zmax.
+ rewrite spec_compare_alt; destruct Zcompare; auto.
+Qed.
+
+Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd.
+Proof. 
+intros x x' Hx y y' Hy.
+rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd.
+Proof.
+intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd.
+Proof.
+intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition.
+Qed.
+
+Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd.
+Proof.
+intros; red; rewrite 2 spec_min; congruence.
+Qed.
+
+Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd.
+Proof.
+intros; red; rewrite 2 spec_max; congruence.
+Qed.
+
+Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Proof.
+intros.
+unfold Z.eq; rewrite spec_lt, spec_le; omega.
+Qed.
+
+Theorem NZlt_irrefl : forall n, ~ n < n.
+Proof.
+intros; rewrite spec_lt; auto with zarith.
+Qed.
+
+Theorem NZlt_succ_r : forall n m, n < (Z.succ m) <-> n <= m.
+Proof.
+intros; rewrite spec_lt, spec_le, Z.spec_succ; omega.
+Qed.
+
+Theorem NZmin_l : forall n m, n <= m -> Z.min n m == n.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_min.
+generalize (Zmin_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmin_r : forall n m, m <= n -> Z.min n m == m.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_min.
+generalize (Zmin_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmax_l : forall n m, m <= n -> Z.max n m == n.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_max.
+generalize (Zmax_spec [n] [m]); omega.
+Qed.
+
+Theorem NZmax_r : forall n m, n <= m -> Z.max n m == m.
+Proof.
+intros n m; unfold Z.eq; rewrite spec_le, spec_max.
+generalize (Zmax_spec [n] [m]); omega.
+Qed.
+
+End NZOrdAxiomsMod.
+
+Definition Zopp := Z.opp.
+
+Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd.
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n.
+Proof.
+red; intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem Zopp_0 : - 0 == 0.
+Proof.
+red; intros; zsimpl; auto with zarith.
+Qed.
+
+Theorem Zopp_succ : forall n, - (Z.succ n) == Z.pred (- n).
+Proof.
+intros; zsimpl; auto with zarith.
+Qed.
+
+End ZSig_ZAxioms.