Imported Upstream version 8.4dfsgupstream/8.4dfsg

7 files changed, 325 insertions, 367 deletions

diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index 3f9d0f44..ea5a8cb7 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,9 +19,9 @@ Require Export OmegaLemmas.
 Require Export PreOmega.
 Declare ML Module "omega_plugin".
 
-Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
-  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
-  Zmult_plus_distr_r: zarith.
+Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
+  Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r
+  Z.mul_add_distr_l: zarith.
 
 Require Export Zhints.
 
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
index 5b6f4670..1872f576 100644
--- a/plugins/omega/OmegaLemmas.v
+++ b/plugins/omega/OmegaLemmas.v
@@ -6,232 +6,192 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import ZArith_base.
-Open Local Scope Z_scope.
+Require Import BinInt Znat.
+Local Open Scope Z_scope.
 
 (** Factorization lemmas *)
 
-Theorem Zred_factor0 : forall n:Z, n = n * 1.
-  intro x; rewrite (Zmult_1_r x); reflexivity.
+Theorem Zred_factor0 n : n = n * 1.
+Proof.
+  now Z.nzsimpl.
 Qed.
 
-Theorem Zred_factor1 : forall n:Z, n + n = n * 2.
+Theorem Zred_factor1 n : n + n = n * 2.
 Proof.
-  exact Zplus_diag_eq_mult_2.
+  rewrite Z.mul_comm. apply Z.add_diag.
 Qed.
 
-Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m).
+Theorem Zred_factor2 n m : n + n * m = n * (1 + m).
 Proof.
-  intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x);
-    rewrite <- Zmult_plus_distr_r; trivial with arith.
+  rewrite Z.mul_add_distr_l; now Z.nzsimpl.
 Qed.
 
-Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m).
+Theorem Zred_factor3 n m : n * m + n = n * (1 + m).
 Proof.
-  intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x);
-    rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm;
-      trivial with arith.
+  now Z.nzsimpl.
 Qed.
 
-Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p).
+Theorem Zred_factor4 n m p : n * m + n * p = n * (m + p).
 Proof.
-  intros x y z; symmetry  in |- *; apply Zmult_plus_distr_r.
+  symmetry; apply Z.mul_add_distr_l.
 Qed.
 
-Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m.
+Theorem Zred_factor5 n m : n * 0 + m = m.
 Proof.
-  intros x y; rewrite <- Zmult_0_r_reverse; auto with arith.
+  now Z.nzsimpl.
 Qed.
 
-Theorem Zred_factor6 : forall n:Z, n = n + 0.
+Theorem Zred_factor6 n : n = n + 0.
 Proof.
-  intro; rewrite Zplus_0_r; trivial with arith.
+  now Z.nzsimpl.
 Qed.
 
 (** Other specific variants of theorems dedicated for the Omega tactic *)
 
 Lemma new_var : forall x : Z, exists y : Z, x = y.
-intros x; exists x; trivial with arith.
+Proof.
+intros x; now exists x.
 Qed.
 
-Lemma OMEGA1 : forall x y : Z, x = y -> 0 <= x -> 0 <= y.
-intros x y H; rewrite H; auto with arith.
+Lemma OMEGA1 x y : x = y -> 0 <= x -> 0 <= y.
+Proof.
+now intros ->.
 Qed.
 
-Lemma OMEGA2 : forall x y : Z, 0 <= x -> 0 <= y -> 0 <= x + y.
-exact Zplus_le_0_compat.
+Lemma OMEGA2 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
+Proof.
+Z.order_pos.
 Qed.
 
-Lemma OMEGA3 : forall x y k : Z, k > 0 -> x = y * k -> x = 0 -> y = 0.
-
-intros x y k H1 H2 H3; apply (Zmult_integral_l k);
- [ unfold not in |- *; intros H4; absurd (k > 0);
-    [ rewrite H4; unfold Zgt in |- *; simpl in |- *; discriminate
-    | assumption ]
- | rewrite <- H2; assumption ].
+Lemma OMEGA3 x y k : k > 0 -> x = y * k -> x = 0 -> y = 0.
+Proof.
+intros LT -> EQ. apply Z.mul_eq_0 in EQ. destruct EQ; now subst.
 Qed.
 
-Lemma OMEGA4 : forall x y z : Z, x > 0 -> y > x -> z * y + x <> 0.
-
-unfold not in |- *; intros x y z H1 H2 H3; cut (y > 0);
- [ intros H4; cut (0 <= z * y + x);
-    [ intros H5; generalize (Zmult_le_approx y z x H4 H2 H5); intros H6;
-       absurd (z * y + x > 0);
-       [ rewrite H3; unfold Zgt in |- *; simpl in |- *; discriminate
-       | apply Zle_gt_trans with x;
-          [ pattern x at 1 in |- *; rewrite <- (Zplus_0_l x);
-             apply Zplus_le_compat_r; rewrite Zmult_comm;
-             generalize H4; unfold Zgt in |- *; case y;
-             [ simpl in |- *; intros H7; discriminate H7
-             | intros p H7; rewrite <- (Zmult_0_r (Zpos p));
-                unfold Zle in |- *; rewrite Zcompare_mult_compat;
-                exact H6
-             | simpl in |- *; intros p H7; discriminate H7 ]
-          | assumption ] ]
-    | rewrite H3; unfold Zle in |- *; simpl in |- *; discriminate ]
- | apply Zgt_trans with x; [ assumption | assumption ] ].
+Lemma OMEGA4 x y z : x > 0 -> y > x -> z * y + x <> 0.
+Proof.
+Z.swap_greater. intros Hx Hxy.
+rewrite Z.add_move_0_l, <- Z.mul_opp_l.
+destruct (Z.lt_trichotomy (-z) 1) as [LT|[->|GT]].
+- intro. revert LT. apply Z.le_ngt, (Z.le_succ_l 0).
+  apply Z.mul_pos_cancel_r with y; Z.order.
+- Z.nzsimpl. Z.order.
+- rewrite (Z.mul_lt_mono_pos_r y), Z.mul_1_l in GT; Z.order.
 Qed.
 
-Lemma OMEGA5 : forall x y z : Z, x = 0 -> y = 0 -> x + y * z = 0.
-
-intros x y z H1 H2; rewrite H1; rewrite H2; simpl in |- *; trivial with arith.
+Lemma OMEGA5 x y z : x = 0 -> y = 0 -> x + y * z = 0.
+Proof.
+now intros -> ->.
 Qed.
 
-Lemma OMEGA6 : forall x y z : Z, 0 <= x -> y = 0 -> 0 <= x + y * z.
-
-intros x y z H1 H2; rewrite H2; simpl in |- *; rewrite Zplus_0_r; assumption.
+Lemma OMEGA6 x y z : 0 <= x -> y = 0 -> 0 <= x + y * z.
+Proof.
+intros H ->. now Z.nzsimpl.
 Qed.
 
-Lemma OMEGA7 :
- forall x y z t : Z, z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t.
-
-intros x y z t H1 H2 H3 H4; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat;
- apply Zmult_gt_0_le_0_compat; assumption.
+Lemma OMEGA7 x y z t :
+ z > 0 -> t > 0 -> 0 <= x -> 0 <= y -> 0 <= x * z + y * t.
+Proof.
+intros. Z.swap_greater. Z.order_pos.
 Qed.
 
-Lemma OMEGA8 : forall x y : Z, 0 <= x -> 0 <= y -> x = - y -> x = 0.
-
-intros x y H1 H2 H3; elim (Zle_lt_or_eq 0 x H1);
- [ intros H4; absurd (0 < x);
-    [ change (0 >= x) in |- *; apply Zle_ge; apply Zplus_le_reg_l with y;
-       rewrite H3; rewrite Zplus_opp_r; rewrite Zplus_0_r;
-       assumption
-    | assumption ]
- | intros H4; rewrite H4; trivial with arith ].
+Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0.
+Proof.
+intros H1 H2 H3. rewrite <- Z.opp_nonpos_nonneg in H2. Z.order.
 Qed.
 
-Lemma OMEGA9 : forall x y z t : Z, y = 0 -> x = z -> y + (- x + z) * t = 0.
-
-intros x y z t H1 H2; rewrite H2; rewrite Zplus_opp_l; rewrite Zmult_0_l;
- rewrite Zplus_0_r; assumption.
+Lemma OMEGA9 x y z t : y = 0 -> x = z -> y + (- x + z) * t = 0.
+Proof.
+intros. subst. now rewrite Z.add_opp_diag_l.
 Qed.
 
-Lemma OMEGA10 :
- forall v c1 c2 l1 l2 k1 k2 : Z,
+Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 :
  (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
  v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
-
-intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
- rewrite (Zplus_permute (l1 * k1) (v * c2 * k2)); trivial with arith.
+Proof.
+rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc.
+rewrite <- !Z.add_assoc. f_equal. apply Z.add_shuffle3.
 Qed.
 
-Lemma OMEGA11 :
- forall v1 c1 l1 l2 k1 : Z,
+Lemma OMEGA11 v1 c1 l1 l2 k1 :
  (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
-
-intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
- trivial with arith.
+Proof.
+rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc.
+now rewrite Z.add_assoc.
 Qed.
 
-Lemma OMEGA12 :
- forall v2 c2 l1 l2 k2 : Z,
+Lemma OMEGA12 v2 c2 l1 l2 k2 :
  l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
-
-intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
- rewrite Zplus_permute; trivial with arith.
+Proof.
+rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc.
+apply Z.add_shuffle3.
 Qed.
 
-Lemma OMEGA13 :
- forall (v l1 l2 : Z) (x : positive),
+Lemma OMEGA13 (v l1 l2 : Z) (x : positive) :
  v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2.
-
-intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zpos x) l1);
- rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
- rewrite <- Zopp_neg; rewrite (Zplus_comm (- Zneg x) (Zneg x));
- rewrite Zplus_opp_r; rewrite Zmult_0_r; rewrite Zplus_0_r;
- trivial with arith.
+Proof.
+ rewrite Z.add_shuffle1.
+ rewrite <- Z.mul_add_distr_l, <- Pos2Z.opp_neg, Z.add_opp_diag_r.
+ now Z.nzsimpl.
 Qed.
 
-Lemma OMEGA14 :
- forall (v l1 l2 : Z) (x : positive),
+Lemma OMEGA14 (v l1 l2 : Z) (x : positive) :
  v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
-
-intros; rewrite Zplus_assoc; rewrite (Zplus_comm (v * Zneg x) l1);
- rewrite (Zplus_assoc_reverse l1); rewrite <- Zmult_plus_distr_r;
- rewrite <- Zopp_neg; rewrite Zplus_opp_r; rewrite Zmult_0_r;
- rewrite Zplus_0_r; trivial with arith.
+Proof.
+ rewrite Z.add_shuffle1.
+ rewrite <- Z.mul_add_distr_l, <- Pos2Z.opp_neg, Z.add_opp_diag_r.
+ now Z.nzsimpl.
 Qed.
-Lemma OMEGA15 :
- forall v c1 c2 l1 l2 k2 : Z,
- v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
 
-intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
- rewrite (Zplus_permute l1 (v * c2 * k2)); trivial with arith.
+Lemma OMEGA15 v c1 c2 l1 l2 k2 :
+ v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
+Proof.
+ rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc.
+ apply Z.add_shuffle1.
 Qed.
 
-Lemma OMEGA16 : forall v c l k : Z, (v * c + l) * k = v * (c * k) + l * k.
-
-intros; repeat rewrite Zmult_plus_distr_l || rewrite Zmult_plus_distr_r;
- repeat rewrite Zmult_assoc; repeat elim Zplus_assoc;
- trivial with arith.
+Lemma OMEGA16 v c l k : (v * c + l) * k = v * (c * k) + l * k.
+Proof.
+ now rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc.
 Qed.
 
-Lemma OMEGA17 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
-
-unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1;
- apply Zplus_reg_l with (y * z); rewrite Zplus_comm;
- rewrite H3; rewrite H2; auto with arith.
+Lemma OMEGA17 x y z : Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
+Proof.
+ unfold Zne, not. intros NE EQ. subst. now Z.nzsimpl.
 Qed.
 
-Lemma OMEGA18 : forall x y k : Z, x = y * k -> Zne x 0 -> Zne y 0.
-
-unfold Zne, not in |- *; intros x y k H1 H2 H3; apply H2; rewrite H1;
- rewrite H3; auto with arith.
+Lemma OMEGA18 x y k : x = y * k -> Zne x 0 -> Zne y 0.
+Proof.
+ unfold Zne, not. intros. subst; auto.
 Qed.
 
-Lemma OMEGA19 : forall x : Z, Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1.
-
-unfold Zne in |- *; intros x H; elim (Zle_or_lt 0 x);
- [ intros H1; elim Zle_lt_or_eq with (1 := H1);
-    [ intros H2; left; change (0 <= Zpred x) in |- *; apply Zsucc_le_reg;
-       rewrite <- Zsucc_pred; apply Zlt_le_succ; assumption
-    | intros H2; absurd (x = 0); auto with arith ]
- | intros H1; right; rewrite <- Zopp_eq_mult_neg_1; rewrite Zplus_comm;
-    apply Zle_left; apply Zsucc_le_reg; simpl in |- *;
-    apply Zlt_le_succ; auto with arith ].
+Lemma OMEGA19 x : Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1.
+Proof.
+ unfold Zne. intros Hx. apply Z.lt_gt_cases in Hx.
+ destruct Hx as [LT|GT].
+ - right. change (-1) with (-(1)).
+   rewrite Z.mul_opp_r, <- Z.opp_add_distr. Z.nzsimpl.
+   rewrite Z.opp_nonneg_nonpos. now apply Z.le_succ_l.
+ - left. now apply Z.lt_le_pred.
 Qed.
 
-Lemma OMEGA20 : forall x y z : Z, Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
-
-unfold Zne, not in |- *; intros x y z H1 H2 H3; apply H1; rewrite H2 in H3;
- simpl in H3; rewrite Zplus_0_r in H3; trivial with arith.
+Lemma OMEGA20 x y z : Zne x 0 -> y = 0 -> Zne (x + y * z) 0.
+Proof.
+ unfold Zne, not. intros H1 H2 H3; apply H1; rewrite H2 in H3;
+ simpl in H3; rewrite Z.add_0_r in H3; trivial with arith.
 Qed.
 
 Definition fast_Zplus_comm (x y : Z) (P : Z -> Prop)
-  (H : P (y + x)) := eq_ind_r P H (Zplus_comm x y).
+  (H : P (y + x)) := eq_ind_r P H (Z.add_comm x y).
 
 Definition fast_Zplus_assoc_reverse (n m p : Z) (P : Z -> Prop)
   (H : P (n + (m + p))) := eq_ind_r P H (Zplus_assoc_reverse n m p).
 
 Definition fast_Zplus_assoc (n m p : Z) (P : Z -> Prop)
-  (H : P (n + m + p)) := eq_ind_r P H (Zplus_assoc n m p).
+  (H : P (n + m + p)) := eq_ind_r P H (Z.add_assoc n m p).
 
 Definition fast_Zplus_permute (n m p : Z) (P : Z -> Prop)
-  (H : P (m + (n + p))) := eq_ind_r P H (Zplus_permute n m p).
+  (H : P (m + (n + p))) := eq_ind_r P H (Z.add_shuffle3 n m p).
 
 Definition fast_OMEGA10 (v c1 c2 l1 l2 k1 k2 : Z) (P : Z -> Prop)
   (H : P (v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2))) :=
@@ -259,24 +219,24 @@ Definition fast_Zred_factor0 (x : Z) (P : Z -> Prop)
   (H : P (x * 1)) := eq_ind_r P H (Zred_factor0 x).
 
 Definition fast_Zopp_eq_mult_neg_1 (x : Z) (P : Z -> Prop)
-  (H : P (x * -1)) := eq_ind_r P H (Zopp_eq_mult_neg_1 x).
+  (H : P (x * -1)) := eq_ind_r P H (Z.opp_eq_mul_m1 x).
 
 Definition fast_Zmult_comm (x y : Z) (P : Z -> Prop)
-  (H : P (y * x)) := eq_ind_r P H (Zmult_comm x y).
+  (H : P (y * x)) := eq_ind_r P H (Z.mul_comm x y).
 
 Definition fast_Zopp_plus_distr (x y : Z) (P : Z -> Prop)
-  (H : P (- x + - y)) := eq_ind_r P H (Zopp_plus_distr x y).
+  (H : P (- x + - y)) := eq_ind_r P H (Z.opp_add_distr x y).
 
 Definition fast_Zopp_involutive (x : Z) (P : Z -> Prop) (H : P x) :=
-  eq_ind_r P H (Zopp_involutive x).
+  eq_ind_r P H (Z.opp_involutive x).
 
 Definition fast_Zopp_mult_distr_r (x y : Z) (P : Z -> Prop)
   (H : P (x * - y)) := eq_ind_r P H (Zopp_mult_distr_r x y).
 
 Definition fast_Zmult_plus_distr_l (n m p : Z) (P : Z -> Prop)
-  (H : P (n * p + m * p)) := eq_ind_r P H (Zmult_plus_distr_l n m p).
+  (H : P (n * p + m * p)) := eq_ind_r P H (Z.mul_add_distr_r n m p).
 Definition fast_Zmult_opp_comm (x y : Z) (P : Z -> Prop)
-  (H : P (x * - y)) := eq_ind_r P H (Zmult_opp_comm x y).
+  (H : P (x * - y)) := eq_ind_r P H (Z.mul_opp_comm x y).
 
 Definition fast_Zmult_assoc_reverse (n m p : Z) (P : Z -> Prop)
   (H : P (n * (m * p))) := eq_ind_r P H (Zmult_assoc_reverse n m p).
@@ -300,8 +260,8 @@ Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop)
   (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x).
 
 Theorem intro_Z :
-  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+  forall n:nat,  exists y : Z, Z.of_nat n = y /\ 0 <= y * 1 + 0.
 Proof.
-  intros n; exists (Z_of_nat n); split; trivial.
-  rewrite Zmult_1_r, Zplus_0_r. apply Zle_0_nat.
+  intros n; exists (Z.of_nat n); split; trivial.
+  rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg.
 Qed.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index a3ab34a9..433db414 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 46fd5682..60e606a6 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -1,6 +1,14 @@
-Require Import Arith Max Min ZArith_base NArith Nnat.
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
-Open Local Scope Z_scope.
+Require Import Arith Max Min BinInt BinNat Znat Nnat.
+
+Local Open Scope Z_scope.
 
 
 (** * zify: the Z-ification tactic *)
@@ -15,16 +23,16 @@ Open Local Scope Z_scope.
      - { eq, le, lt, ge, gt } on { Z, positive, N, nat }
 
    Recognized operations:
-     - on Z: Zmin, Zmax, Zabs, Zsgn are translated in term of <= < =
-     - on nat: + * - S O pred min max nat_of_P nat_of_N Zabs_nat
-     - on positive: Zneg Zpos xI xO xH + * - Psucc Ppred Pmin Pmax P_of_succ_nat
-     - on N: N0 Npos + * - Nsucc Nmin Nmax N_of_nat Zabs_N
+     - on Z: Z.min, Z.max, Z.abs, Z.sgn are translated in term of <= < =
+     - on nat: + * - S O pred min max Pos.to_nat N.to_nat Z.abs_nat
+     - on positive: Zneg Zpos xI xO xH + * - Pos.succ Pos.pred Pos.min Pos.max Pos.of_succ_nat
+     - on N: N0 Npos + * - N.succ N.min N.max N.of_nat Z.abs_N
 *)
 
 
 
 
-(** I) translation of Zmax, Zmin, Zabs, Zsgn into recognized equations *)
+(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *)
 
 Ltac zify_unop_core t thm a :=
  (* Let's introduce the specification theorem for t *)
@@ -48,7 +56,7 @@ Ltac zify_unop t thm a :=
  end.
 
 Ltac zify_unop_nored t thm a :=
- (* in this version, we don't try to reduce the unop (that can be (Zplus x)) *)
+ (* in this version, we don't try to reduce the unop (that can be (Z.add x)) *)
  let isz := isZcst a in
  match isz with
   | true => zify_unop_core t thm a
@@ -72,14 +80,14 @@ Ltac zify_binop t thm a b:=
 
 Ltac zify_op_1 :=
   match goal with
-   | |- context [ Zmax ?a ?b ] => zify_binop Zmax Zmax_spec a b
-   | H : context [ Zmax ?a ?b ] |- _ => zify_binop Zmax Zmax_spec a b
-   | |- context [ Zmin ?a ?b ] => zify_binop Zmin Zmin_spec a b
-   | H : context [ Zmin ?a ?b ] |- _ => zify_binop Zmin Zmin_spec a b
-   | |- context [ Zsgn ?a ] => zify_unop Zsgn Zsgn_spec a
-   | H : context [ Zsgn ?a ] |- _ => zify_unop Zsgn Zsgn_spec a
-   | |- context [ Zabs ?a ] => zify_unop Zabs Zabs_spec a
-   | H : context [ Zabs ?a ] |- _ => zify_unop Zabs Zabs_spec a
+   | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b
+   | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b
+   | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b
+   | H : context [ Z.min ?a ?b ] |- _ => zify_binop Z.min Z.min_spec a b
+   | |- context [ Z.sgn ?a ] => zify_unop Z.sgn Z.sgn_spec a
+   | H : context [ Z.sgn ?a ] |- _ => zify_unop Z.sgn Z.sgn_spec a
+   | |- context [ Z.abs ?a ] => zify_unop Z.abs Z.abs_spec a
+   | H : context [ Z.abs ?a ] |- _ => zify_unop Z.abs Z.abs_spec a
   end.
 
 Ltac zify_op := repeat zify_op_1.
@@ -91,100 +99,95 @@ Ltac zify_op := repeat zify_op_1.
 (** II) Conversion from nat to Z *)
 
 
-Definition Z_of_nat' := Z_of_nat.
+Definition Z_of_nat' := Z.of_nat.
 
 Ltac hide_Z_of_nat t :=
-  let z := fresh "z" in set (z:=Z_of_nat t) in *;
-  change Z_of_nat with Z_of_nat' in z;
+  let z := fresh "z" in set (z:=Z.of_nat t) in *;
+  change Z.of_nat with Z_of_nat' in z;
   unfold z in *; clear z.
 
 Ltac zify_nat_rel :=
  match goal with
   (* I: equalities *)
-  | H : (@eq nat ?a ?b) |- _ => generalize (inj_eq _ _ H); clear H; intro H
-  | |- (@eq nat ?a ?b) => apply (inj_eq_rev a b)
-  | H : context [ @eq nat ?a ?b ] |- _ => rewrite (inj_eq_iff a b) in H
-  | |- context [ @eq nat ?a ?b ] =>       rewrite (inj_eq_iff a b)
+  | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *)
+  | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H
+  | |- context [ @eq nat ?a ?b ] =>       rewrite <- (Nat2Z.inj_iff a b)
   (* II: less than *)
-  | H : (lt ?a ?b) |- _ => generalize (inj_lt _ _ H); clear H; intro H
-  | |- (lt ?a ?b) => apply (inj_lt_rev a b)
-  | H : context [ lt ?a ?b ] |- _ => rewrite (inj_lt_iff a b) in H
-  | |- context [ lt ?a ?b ] =>       rewrite (inj_lt_iff a b)
+  | H : context [ lt ?a ?b ] |- _ => rewrite (Nat2Z.inj_lt a b) in H
+  | |- context [ lt ?a ?b ] =>       rewrite (Nat2Z.inj_lt a b)
   (* III: less or equal *)
-  | H : (le ?a ?b) |- _ => generalize (inj_le _ _ H); clear H; intro H
-  | |- (le ?a ?b) => apply (inj_le_rev a b)
-  | H : context [ le ?a ?b ] |- _ => rewrite (inj_le_iff a b) in H
-  | |- context [ le ?a ?b ] =>       rewrite (inj_le_iff a b)
+  | H : context [ le ?a ?b ] |- _ => rewrite (Nat2Z.inj_le a b) in H
+  | |- context [ le ?a ?b ] =>       rewrite (Nat2Z.inj_le a b)
   (* IV: greater than *)
-  | H : (gt ?a ?b) |- _ => generalize (inj_gt _ _ H); clear H; intro H
-  | |- (gt ?a ?b) => apply (inj_gt_rev a b)
-  | H : context [ gt ?a ?b ] |- _ => rewrite (inj_gt_iff a b) in H
-  | |- context [ gt ?a ?b ] =>       rewrite (inj_gt_iff a b)
+  | H : context [ gt ?a ?b ] |- _ => rewrite (Nat2Z.inj_gt a b) in H
+  | |- context [ gt ?a ?b ] =>       rewrite (Nat2Z.inj_gt a b)
   (* V: greater or equal *)
-  | H : (ge ?a ?b) |- _ => generalize (inj_ge _ _ H); clear H; intro H
-  | |- (ge ?a ?b) => apply (inj_ge_rev a b)
-  | H : context [ ge ?a ?b ] |- _ => rewrite (inj_ge_iff a b) in H
-  | |- context [ ge ?a ?b ] =>       rewrite (inj_ge_iff a b)
+  | H : context [ ge ?a ?b ] |- _ => rewrite (Nat2Z.inj_ge a b) in H
+  | |- context [ ge ?a ?b ] =>       rewrite (Nat2Z.inj_ge a b)
  end.
 
 Ltac zify_nat_op :=
  match goal with
   (* misc type conversions: positive/N/Z to nat *)
-  | H : context [ Z_of_nat (nat_of_P ?a) ] |- _ => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a) in H
-  | |- context [ Z_of_nat (nat_of_P ?a) ] => rewrite <- (Zpos_eq_Z_of_nat_o_nat_of_P a)
-  | H : context [ Z_of_nat (nat_of_N ?a) ] |- _ => rewrite (Z_of_nat_of_N a) in H
-  | |- context [ Z_of_nat (nat_of_N ?a) ] => rewrite (Z_of_nat_of_N a)
-  | H : context [ Z_of_nat (Zabs_nat ?a) ] |- _ => rewrite (inj_Zabs_nat a) in H
-  | |- context [ Z_of_nat (Zabs_nat ?a) ] => rewrite (inj_Zabs_nat a)
-
-  (* plus -> Zplus *)
-  | H : context [ Z_of_nat (plus ?a ?b) ] |- _ => rewrite (inj_plus a b) in H
-  | |- context [ Z_of_nat (plus ?a ?b) ] => rewrite (inj_plus a b)
-
-  (* min -> Zmin *)
-  | H : context [ Z_of_nat (min ?a ?b) ] |- _ => rewrite (inj_min a b) in H
-  | |- context [ Z_of_nat (min ?a ?b) ] => rewrite (inj_min a b)
-
-  (* max -> Zmax *)
-  | H : context [ Z_of_nat (max ?a ?b) ] |- _ => rewrite (inj_max a b) in H
-  | |- context [ Z_of_nat (max ?a ?b) ] => rewrite (inj_max a b)
-
-  (* minus -> Zmax (Zminus ... ...) 0 *)
-  | H : context [ Z_of_nat (minus ?a ?b) ] |- _ => rewrite (inj_minus a b) in H
-  | |- context [ Z_of_nat (minus ?a ?b) ] => rewrite (inj_minus a b)
-
-  (* pred -> minus ... -1 -> Zmax (Zminus ... -1) 0 *)
-  | H : context [ Z_of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H
-  | |- context [ Z_of_nat (pred ?a) ] => rewrite (pred_of_minus a)
-
-  (* mult -> Zmult and a positivity hypothesis *)
-  | H : context [ Z_of_nat (mult ?a ?b) ] |- _ =>
-        pose proof (Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
-  | |- context [ Z_of_nat (mult ?a ?b) ] =>
-        pose proof (Zle_0_nat (mult a b)); rewrite (inj_mult a b) in *
+  | H : context [ Z.of_nat (Pos.to_nat ?a) ] |- _ => rewrite (positive_nat_Z a) in H
+  | |- context [ Z.of_nat (Pos.to_nat ?a) ] => rewrite (positive_nat_Z a)
+  | H : context [ Z.of_nat (N.to_nat ?a) ] |- _ => rewrite (N_nat_Z a) in H
+  | |- context [ Z.of_nat (N.to_nat ?a) ] => rewrite (N_nat_Z a)
+  | H : context [ Z.of_nat (Z.abs_nat ?a) ] |- _ => rewrite (Zabs2Nat.id_abs a) in H
+  | |- context [ Z.of_nat (Z.abs_nat ?a) ] => rewrite (Zabs2Nat.id_abs a)
+
+  (* plus -> Z.add *)
+  | H : context [ Z.of_nat (plus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_add a b) in H
+  | |- context [ Z.of_nat (plus ?a ?b) ] => rewrite (Nat2Z.inj_add a b)
+
+  (* min -> Z.min *)
+  | H : context [ Z.of_nat (min ?a ?b) ] |- _ => rewrite (Nat2Z.inj_min a b) in H
+  | |- context [ Z.of_nat (min ?a ?b) ] => rewrite (Nat2Z.inj_min a b)
+
+  (* max -> Z.max *)
+  | H : context [ Z.of_nat (max ?a ?b) ] |- _ => rewrite (Nat2Z.inj_max a b) in H
+  | |- context [ Z.of_nat (max ?a ?b) ] => rewrite (Nat2Z.inj_max a b)
+
+  (* minus -> Z.max (Z.sub ... ...) 0 *)
+  | H : context [ Z.of_nat (minus ?a ?b) ] |- _ => rewrite (Nat2Z.inj_sub_max a b) in H
+  | |- context [ Z.of_nat (minus ?a ?b) ] => rewrite (Nat2Z.inj_sub_max a b)
+
+  (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *)
+  | H : context [ Z.of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H
+  | |- context [ Z.of_nat (pred ?a) ] => rewrite (pred_of_minus a)
+
+  (* mult -> Z.mul and a positivity hypothesis *)
+  | H : context [ Z.of_nat (mult ?a ?b) ] |- _ =>
+        pose proof (Nat2Z.is_nonneg (mult a b));
+        rewrite (Nat2Z.inj_mul a b) in *
+  | |- context [ Z.of_nat (mult ?a ?b) ] =>
+        pose proof (Nat2Z.is_nonneg (mult a b));
+        rewrite (Nat2Z.inj_mul a b) in *
 
   (* O -> Z0 *)
-  | H : context [ Z_of_nat O ] |- _ => simpl (Z_of_nat O) in H
-  | |- context [ Z_of_nat O ] => simpl (Z_of_nat O)
+  | H : context [ Z.of_nat O ] |- _ => simpl (Z.of_nat O) in H
+  | |- context [ Z.of_nat O ] => simpl (Z.of_nat O)
 
-  (* S -> number or Zsucc *)
-  | H : context [ Z_of_nat (S ?a) ] |- _ =>
+  (* S -> number or Z.succ *)
+  | H : context [ Z.of_nat (S ?a) ] |- _ =>
      let isnat := isnatcst a in
      match isnat with
-      | true => simpl (Z_of_nat (S a)) in H
-      | _ => rewrite (inj_S a) in H
+      | true => simpl (Z.of_nat (S a)) in H
+      | _ => rewrite (Nat2Z.inj_succ a) in H
      end
-  | |- context [ Z_of_nat (S ?a) ] =>
+  | |- context [ Z.of_nat (S ?a) ] =>
      let isnat := isnatcst a in
      match isnat with
-      | true => simpl (Z_of_nat (S a))
-      | _ => rewrite (inj_S a)
+      | true => simpl (Z.of_nat (S a))
+      | _ => rewrite (Nat2Z.inj_succ a)
      end
 
   (* atoms of type nat : we add a positivity condition (if not already there) *)
-  | _ : 0 <= Z_of_nat ?a |- _ => hide_Z_of_nat a
-  | _ : context [ Z_of_nat ?a ] |- _ => pose proof (Zle_0_nat a); hide_Z_of_nat a
-  | |- context [ Z_of_nat ?a ] => pose proof (Zle_0_nat a); hide_Z_of_nat a
+  | _ : 0 <= Z.of_nat ?a |- _ => hide_Z_of_nat a
+  | _ : context [ Z.of_nat ?a ] |- _ =>
+    pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a
+  | |- context [ Z.of_nat ?a ] =>
+    pose proof (Nat2Z.is_nonneg a); hide_Z_of_nat a
  end.
 
 Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *.
@@ -205,10 +208,9 @@ Ltac hide_Zpos t :=
 Ltac zify_positive_rel :=
  match goal with
   (* I: equalities *)
-  | H : (@eq positive ?a ?b) |- _ => generalize (Zpos_eq _ _ H); clear H; intro H
-  | |- (@eq positive ?a ?b) => apply (Zpos_eq_rev a b)
-  | H : context [ @eq positive ?a ?b ] |- _ => rewrite (Zpos_eq_iff a b) in H
-  | |- context [ @eq positive ?a ?b ] =>       rewrite (Zpos_eq_iff a b)
+  | |- (@eq positive ?a ?b) => apply Pos2Z.inj
+  | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H
+  | |- context [ @eq positive ?a ?b ] =>       rewrite <- (Pos2Z.inj_iff a b)
   (* II: less than *)
   | H : context [ (?a < ?b)%positive ] |- _ => change (a<b)%positive with (Zpos a<Zpos b) in H
   | |- context [ (?a < ?b)%positive ] => change (a<b)%positive with (Zpos a<Zpos b)
@@ -240,64 +242,66 @@ Ltac zify_positive_op :=
      end
 
   (* misc type conversions: nat to positive *)
-  | H : context [ Zpos (P_of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H
-  | |- context [ Zpos (P_of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a)
+  | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H
+  | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a)
 
-  (* Pplus -> Zplus *)
-  | H : context [ Zpos (Pplus ?a ?b) ] |- _ => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b)) in H
-  | |- context [ Zpos (Pplus ?a ?b) ] => change (Zpos (Pplus a b)) with (Zplus (Zpos a) (Zpos b))
+  (* Pos.add -> Z.add *)
+  | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H
+  | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b)
 
-  (* Pmin -> Zmin *)
-  | H : context [ Zpos (Pmin ?a ?b) ] |- _ => rewrite (Zpos_min a b) in H
-  | |- context [ Zpos (Pmin ?a ?b) ] => rewrite (Zpos_min a b)
+  (* Pos.min -> Z.min *)
+  | H : context [ Zpos (Pos.min ?a ?b) ] |- _ => rewrite (Pos2Z.inj_min a b) in H
+  | |- context [ Zpos (Pos.min ?a ?b) ] => rewrite (Pos2Z.inj_min a b)
 
-  (* Pmax -> Zmax *)
-  | H : context [ Zpos (Pmax ?a ?b) ] |- _ => rewrite (Zpos_max a b) in H
-  | |- context [ Zpos (Pmax ?a ?b) ] => rewrite (Zpos_max a b)
+  (* Pos.max -> Z.max *)
+  | H : context [ Zpos (Pos.max ?a ?b) ] |- _ => rewrite (Pos2Z.inj_max a b) in H
+  | |- context [ Zpos (Pos.max ?a ?b) ] => rewrite (Pos2Z.inj_max a b)
 
-  (* Pminus -> Zmax 1 (Zminus ... ...) *)
-  | H : context [ Zpos (Pminus ?a ?b) ] |- _ => rewrite (Zpos_minus a b) in H
-  | |- context [ Zpos (Pminus ?a ?b) ] => rewrite (Zpos_minus a b)
+  (* Pos.sub -> Z.max 1 (Z.sub ... ...) *)
+  | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub a b) in H
+  | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub a b)
 
-  (* Psucc -> Zsucc *)
-  | H : context [ Zpos (Psucc ?a) ] |- _ => rewrite (Zpos_succ_morphism a) in H
-  | |- context [ Zpos (Psucc ?a) ] => rewrite (Zpos_succ_morphism a)
+  (* Pos.succ -> Z.succ *)
+  | H : context [ Zpos (Pos.succ ?a) ] |- _ => rewrite (Pos2Z.inj_succ a) in H
+  | |- context [ Zpos (Pos.succ ?a) ] => rewrite (Pos2Z.inj_succ a)
 
-  (* Ppred -> Pminus ... -1 -> Zmax 1 (Zminus ... - 1) *)
-  | H : context [ Zpos (Ppred ?a) ] |- _ => rewrite (Ppred_minus a) in H
-  | |- context [ Zpos (Ppred ?a) ] => rewrite (Ppred_minus a)
+  (* Pos.pred -> Pos.sub ... -1 -> Z.max 1 (Z.sub ... - 1) *)
+  | H : context [ Zpos (Pos.pred ?a) ] |- _ => rewrite <- (Pos.sub_1_r a) in H
+  | |- context [ Zpos (Pos.pred ?a) ] => rewrite <- (Pos.sub_1_r a)
 
-  (* Pmult -> Zmult and a positivity hypothesis *)
-  | H : context [ Zpos (Pmult ?a ?b) ] |- _ =>
-        pose proof (Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
-  | |- context [ Zpos (Pmult ?a ?b) ] =>
-        pose proof (Zgt_pos_0 (Pmult a b)); rewrite (Zpos_mult_morphism a b) in *
+  (* Pos.mul -> Z.mul and a positivity hypothesis *)
+  | H : context [ Zpos (?a * ?b) ] |- _ =>
+        pose proof (Pos2Z.is_pos (Pos.mul a b));
+        change (Zpos (a*b)) with (Zpos a * Zpos b) in *
+  | |- context [ Zpos (?a * ?b) ] =>
+        pose proof (Pos2Z.is_pos (Pos.mul a b));
+        change (Zpos (a*b)) with (Zpos a * Zpos b) in *
 
   (* xO *)
   | H : context [ Zpos (xO ?a) ] |- _ =>
      let isp := isPcst a in
      match isp with
       | true => change (Zpos (xO a)) with (Zpos' (xO a)) in H
-      | _ => rewrite (Zpos_xO a) in H
+      | _ => rewrite (Pos2Z.inj_xO a) in H
      end
   | |- context [ Zpos (xO ?a) ] =>
      let isp := isPcst a in
      match isp with
       | true => change (Zpos (xO a)) with (Zpos' (xO a))
-      | _ => rewrite (Zpos_xO a)
+      | _ => rewrite (Pos2Z.inj_xO a)
      end
   (* xI *)
   | H : context [ Zpos (xI ?a) ] |- _ =>
      let isp := isPcst a in
      match isp with
       | true => change (Zpos (xI a)) with (Zpos' (xI a)) in H
-      | _ => rewrite (Zpos_xI a) in H
+      | _ => rewrite (Pos2Z.inj_xI a) in H
      end
   | |- context [ Zpos (xI ?a) ] =>
      let isp := isPcst a in
      match isp with
       | true => change (Zpos (xI a)) with (Zpos' (xI a))
-      | _ => rewrite (Zpos_xI a)
+      | _ => rewrite (Pos2Z.inj_xI a)
      end
 
   (* xI : nothing to do, just prevent adding a useless positivity condition *)
@@ -305,9 +309,9 @@ Ltac zify_positive_op :=
   | |- context [ Zpos xH ] => hide_Zpos xH
 
   (* atoms of type positive : we add a positivity condition (if not already there) *)
-  | _ : Zpos ?a > 0 |- _ => hide_Zpos a
-  | _ : context [ Zpos ?a ] |- _ => pose proof (Zgt_pos_0 a); hide_Zpos a
-  | |- context [ Zpos ?a ] => pose proof (Zgt_pos_0 a); hide_Zpos a
+  | _ : 0 < Zpos ?a |- _ => hide_Zpos a
+  | _ : context [ Zpos ?a ] |- _ => pose proof (Pos2Z.is_pos a); hide_Zpos a
+  | |- context [ Zpos ?a ] => pose proof (Pos2Z.is_pos a); hide_Zpos a
  end.
 
 Ltac zify_positive :=
@@ -319,84 +323,75 @@ Ltac zify_positive :=
 
 (* IV) conversion from N to Z *)
 
-Definition Z_of_N' := Z_of_N.
+Definition Z_of_N' := Z.of_N.
 
 Ltac hide_Z_of_N t :=
-  let z := fresh "z" in set (z:=Z_of_N t) in *;
-  change Z_of_N with Z_of_N' in z;
+  let z := fresh "z" in set (z:=Z.of_N t) in *;
+  change Z.of_N with Z_of_N' in z;
   unfold z in *; clear z.
 
 Ltac zify_N_rel :=
  match goal with
   (* I: equalities *)
-  | H : (@eq N ?a ?b) |- _ => generalize (Z_of_N_eq _ _ H); clear H; intro H
-  | |- (@eq N ?a ?b) => apply (Z_of_N_eq_rev a b)
-  | H : context [ @eq N ?a ?b ] |- _ => rewrite (Z_of_N_eq_iff a b) in H
-  | |- context [ @eq N ?a ?b ] =>       rewrite (Z_of_N_eq_iff a b)
+  | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *)
+  | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H
+  | |- context [ @eq N ?a ?b ] =>       rewrite <- (N2Z.inj_iff a b)
   (* II: less than *)
-  | H : (?a < ?b)%N |- _ => generalize (Z_of_N_lt _ _ H); clear H; intro H
-  | |- (?a < ?b)%N => apply (Z_of_N_lt_rev a b)
-  | H : context [ (?a < ?b)%N ] |- _ => rewrite (Z_of_N_lt_iff a b) in H
-  | |- context [ (?a < ?b)%N ] =>       rewrite (Z_of_N_lt_iff a b)
+  | H : context [ (?a < ?b)%N ] |- _ => rewrite (N2Z.inj_lt a b) in H
+  | |- context [ (?a < ?b)%N ] =>       rewrite (N2Z.inj_lt a b)
   (* III: less or equal *)
-  | H : (?a <= ?b)%N |- _ => generalize (Z_of_N_le _ _ H); clear H; intro H
-  | |- (?a <= ?b)%N => apply (Z_of_N_le_rev a b)
-  | H : context [ (?a <= ?b)%N ] |- _ => rewrite (Z_of_N_le_iff a b) in H
-  | |- context [ (?a <= ?b)%N ] =>       rewrite (Z_of_N_le_iff a b)
+  | H : context [ (?a <= ?b)%N ] |- _ => rewrite (N2Z.inj_le a b) in H
+  | |- context [ (?a <= ?b)%N ] =>       rewrite (N2Z.inj_le a b)
   (* IV: greater than *)
-  | H : (?a > ?b)%N |- _ => generalize (Z_of_N_gt _ _ H); clear H; intro H
-  | |- (?a > ?b)%N => apply (Z_of_N_gt_rev a b)
-  | H : context [ (?a > ?b)%N ] |- _ => rewrite (Z_of_N_gt_iff a b) in H
-  | |- context [ (?a > ?b)%N ] =>       rewrite (Z_of_N_gt_iff a b)
+  | H : context [ (?a > ?b)%N ] |- _ => rewrite (N2Z.inj_gt a b) in H
+  | |- context [ (?a > ?b)%N ] =>       rewrite (N2Z.inj_gt a b)
   (* V: greater or equal *)
-  | H : (?a >= ?b)%N |- _ => generalize (Z_of_N_ge _ _ H); clear H; intro H
-  | |- (?a >= ?b)%N => apply (Z_of_N_ge_rev a b)
-  | H : context [ (?a >= ?b)%N ] |- _ => rewrite (Z_of_N_ge_iff a b) in H
-  | |- context [ (?a >= ?b)%N ] =>       rewrite (Z_of_N_ge_iff a b)
+  | H : context [ (?a >= ?b)%N ] |- _ => rewrite (N2Z.inj_ge a b) in H
+  | |- context [ (?a >= ?b)%N ] =>       rewrite (N2Z.inj_ge a b)
  end.
 
 Ltac zify_N_op :=
  match goal with
   (* misc type conversions: nat to positive *)
-  | H : context [ Z_of_N (N_of_nat ?a) ] |- _ => rewrite (Z_of_N_of_nat a) in H
-  | |- context [ Z_of_N (N_of_nat ?a) ] => rewrite (Z_of_N_of_nat a)
-  | H : context [ Z_of_N (Zabs_N ?a) ] |- _ => rewrite (Z_of_N_abs a) in H
-  | |- context [ Z_of_N (Zabs_N ?a) ] => rewrite (Z_of_N_abs a)
-  | H : context [ Z_of_N (Npos ?a) ] |- _ => rewrite (Z_of_N_pos a) in H
-  | |- context [ Z_of_N (Npos ?a) ] => rewrite (Z_of_N_pos a)
-  | H : context [ Z_of_N N0 ] |- _ => change (Z_of_N N0) with Z0 in H
-  | |- context [ Z_of_N N0 ] => change (Z_of_N N0) with Z0
-
-  (* Nplus -> Zplus *)
-  | H : context [ Z_of_N (Nplus ?a ?b) ] |- _ => rewrite (Z_of_N_plus a b) in H
-  | |- context [ Z_of_N (Nplus ?a ?b) ] => rewrite (Z_of_N_plus a b)
-
-  (* Nmin -> Zmin *)
-  | H : context [ Z_of_N (Nmin ?a ?b) ] |- _ => rewrite (Z_of_N_min a b) in H
-  | |- context [ Z_of_N (Nmin ?a ?b) ] => rewrite (Z_of_N_min a b)
-
-  (* Nmax -> Zmax *)
-  | H : context [ Z_of_N (Nmax ?a ?b) ] |- _ => rewrite (Z_of_N_max a b) in H
-  | |- context [ Z_of_N (Nmax ?a ?b) ] => rewrite (Z_of_N_max a b)
-
-  (* Nminus -> Zmax 0 (Zminus ... ...) *)
-  | H : context [ Z_of_N (Nminus ?a ?b) ] |- _ => rewrite (Z_of_N_minus a b) in H
-  | |- context [ Z_of_N (Nminus ?a ?b) ] => rewrite (Z_of_N_minus a b)
-
-  (* Nsucc -> Zsucc *)
-  | H : context [ Z_of_N (Nsucc ?a) ] |- _ => rewrite (Z_of_N_succ a) in H
-  | |- context [ Z_of_N (Nsucc ?a) ] => rewrite (Z_of_N_succ a)
-
-  (* Nmult -> Zmult and a positivity hypothesis *)
-  | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ =>
-        pose proof (Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
-  | |- context [ Z_of_N  (Nmult ?a ?b) ] =>
-        pose proof (Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in *
+  | H : context [ Z.of_N (N.of_nat ?a) ] |- _ => rewrite (nat_N_Z a) in H
+  | |- context [ Z.of_N (N.of_nat ?a) ] => rewrite (nat_N_Z a)
+  | H : context [ Z.of_N (Z.abs_N ?a) ] |- _ => rewrite (N2Z.inj_abs_N a) in H
+  | |- context [ Z.of_N (Z.abs_N ?a) ] => rewrite (N2Z.inj_abs_N a)
+  | H : context [ Z.of_N (Npos ?a) ] |- _ => rewrite (N2Z.inj_pos a) in H
+  | |- context [ Z.of_N (Npos ?a) ] => rewrite (N2Z.inj_pos a)
+  | H : context [ Z.of_N N0 ] |- _ => change (Z.of_N N0) with Z0 in H
+  | |- context [ Z.of_N N0 ] => change (Z.of_N N0) with Z0
+
+  (* N.add -> Z.add *)
+  | H : context [ Z.of_N (N.add ?a ?b) ] |- _ => rewrite (N2Z.inj_add a b) in H
+  | |- context [ Z.of_N (N.add ?a ?b) ] => rewrite (N2Z.inj_add a b)
+
+  (* N.min -> Z.min *)
+  | H : context [ Z.of_N (N.min ?a ?b) ] |- _ => rewrite (N2Z.inj_min a b) in H
+  | |- context [ Z.of_N (N.min ?a ?b) ] => rewrite (N2Z.inj_min a b)
+
+  (* N.max -> Z.max *)
+  | H : context [ Z.of_N (N.max ?a ?b) ] |- _ => rewrite (N2Z.inj_max a b) in H
+  | |- context [ Z.of_N (N.max ?a ?b) ] => rewrite (N2Z.inj_max a b)
+
+  (* N.sub -> Z.max 0 (Z.sub ... ...) *)
+  | H : context [ Z.of_N (N.sub ?a ?b) ] |- _ => rewrite (N2Z.inj_sub_max a b) in H
+  | |- context [ Z.of_N (N.sub ?a ?b) ] => rewrite (N2Z.inj_sub_max a b)
+
+  (* N.succ -> Z.succ *)
+  | H : context [ Z.of_N (N.succ ?a) ] |- _ => rewrite (N2Z.inj_succ a) in H
+  | |- context [ Z.of_N (N.succ ?a) ] => rewrite (N2Z.inj_succ a)
+
+  (* N.mul -> Z.mul and a positivity hypothesis *)
+  | H : context [ Z.of_N (N.mul ?a ?b) ] |- _ =>
+        pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in *
+  | |- context [ Z.of_N  (N.mul ?a ?b) ] =>
+        pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in *
 
   (* atoms of type N : we add a positivity condition (if not already there) *)
-  | _ : 0 <= Z_of_N ?a |- _ => hide_Z_of_N a
-  | _ : context [ Z_of_N ?a ] |- _ => pose proof (Z_of_N_le_0 a); hide_Z_of_N a
-  | |- context [ Z_of_N ?a ] => pose proof (Z_of_N_le_0 a); hide_Z_of_N a
+  | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a
+  | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a
+  | |- context [ Z.of_N ?a ] => pose proof (N2Z.is_nonneg a); hide_Z_of_N a
  end.
 
 Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d7dfe149..028ef95d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -170,6 +170,9 @@ let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
 let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]]
+let zbase_constant =
+  gen_constant_in_modules "Omega" [["Coq";"ZArith";"BinInt"]]
+
 
 (* Zarith *)
 let coq_xH = lazy (constant "xH")
@@ -181,20 +184,20 @@ let coq_Zneg = lazy (constant "Zneg")
 let coq_Z = lazy (constant "Z")
 let coq_comparison = lazy (constant "comparison")
 let coq_Gt = lazy (constant "Gt")
-let coq_Zplus = lazy (constant "Zplus")
-let coq_Zmult = lazy (constant "Zmult")
-let coq_Zopp = lazy (constant "Zopp")
-let coq_Zminus = lazy (constant "Zminus")
-let coq_Zsucc = lazy (constant "Zsucc")
-let coq_Zpred = lazy (constant "Zpred")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zle = lazy (constant "Zle")
-let coq_Z_of_nat = lazy (constant "Z_of_nat")
-let coq_inj_plus = lazy (constant "inj_plus")
-let coq_inj_mult = lazy (constant "inj_mult")
-let coq_inj_minus1 = lazy (constant "inj_minus1")
+let coq_Zplus = lazy (zbase_constant "Z.add")
+let coq_Zmult = lazy (zbase_constant "Z.mul")
+let coq_Zopp = lazy (zbase_constant "Z.opp")
+let coq_Zminus = lazy (zbase_constant "Z.sub")
+let coq_Zsucc = lazy (zbase_constant "Z.succ")
+let coq_Zpred = lazy (zbase_constant "Z.pred")
+let coq_Zgt = lazy (zbase_constant "Z.gt")
+let coq_Zle = lazy (zbase_constant "Z.le")
+let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat")
+let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add")
+let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul")
+let coq_inj_minus1 = lazy (z_constant "Nat2Z.inj_sub")
 let coq_inj_minus2 = lazy (constant "inj_minus2")
-let coq_inj_S = lazy (z_constant "inj_S")
+let coq_inj_S = lazy (z_constant "Nat2Z.inj_succ")
 let coq_inj_le = lazy (z_constant "Znat.inj_le")
 let coq_inj_lt = lazy (z_constant "Znat.inj_lt")
 let coq_inj_ge = lazy (z_constant "Znat.inj_ge")
@@ -250,10 +253,10 @@ let coq_Zle_left = lazy (constant "Zle_left")
 let coq_new_var = lazy (constant "new_var")
 let coq_intro_Z = lazy (constant "intro_Z")
 
-let coq_dec_eq = lazy (constant "dec_eq")
+let coq_dec_eq = lazy (zbase_constant "Z.eq_decidable")
 let coq_dec_Zne = lazy (constant "dec_Zne")
-let coq_dec_Zle = lazy (constant "dec_Zle")
-let coq_dec_Zlt = lazy (constant "dec_Zlt")
+let coq_dec_Zle = lazy (zbase_constant "Z.le_decidable")
+let coq_dec_Zlt = lazy (zbase_constant "Z.lt_decidable")
 let coq_dec_Zgt = lazy (constant "dec_Zgt")
 let coq_dec_Zge = lazy (constant "dec_Zge")
 
@@ -265,10 +268,10 @@ let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
 let coq_Znot_gt_le = lazy (constant "Znot_gt_le")
 let coq_neq = lazy (constant "neq")
 let coq_Zne = lazy (constant "Zne")
-let coq_Zle = lazy (constant "Zle")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zge = lazy (constant "Zge")
-let coq_Zlt = lazy (constant "Zlt")
+let coq_Zle = lazy (zbase_constant "Z.le")
+let coq_Zgt = lazy (zbase_constant "Z.gt")
+let coq_Zge = lazy (zbase_constant "Z.ge")
+let coq_Zlt = lazy (zbase_constant "Z.lt")
 
 (* Peano/Datatypes *)
 let coq_le = lazy (init_constant "le")
@@ -326,13 +329,13 @@ let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
       EvalConstRef kn
   | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
 
-let sp_Zsucc =     lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
-let sp_Zpred =     lazy (evaluable_ref_of_constr "Zpred" coq_Zpred)
-let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
-let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
-let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
-let sp_Zge = lazy (evaluable_ref_of_constr "Zge" coq_Zge)
-let sp_Zlt = lazy (evaluable_ref_of_constr "Zlt" coq_Zlt)
+let sp_Zsucc =     lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc)
+let sp_Zpred =     lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred)
+let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus)
+let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle)
+let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt)
+let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge)
+let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt)
 let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ())))
 
 let mk_var v = mkVar (id_of_string v)
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 84cc8464..1542b60c 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 3a5aece7..98cad09e 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)