Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.

Reviewed-by: Zimmi48

5 files changed, 0 insertions, 984 deletions

diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
deleted file mode 100644
index 4ceb530827..0000000000
--- a/plugins/omega/Omega.v
+++ /dev/null
@@ -1,55 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-(**************************************************************************)
-(*                                                                        *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
-(*                                                                        *)
-(* Pierre Crégut (CNET, Lannion, France)                                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* We import what is necessary for Omega *)
-Require Export ZArith_base.
-Require Export OmegaLemmas.
-Require Export PreOmega.
-
-Declare ML Module "omega_plugin".
-
-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.
-
-Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
-Hint Extern 10 (_ <= _) => abstract omega: zarith.
-Hint Extern 10 (_ < _) => abstract omega: zarith.
-Hint Extern 10 (_ >= _) => abstract omega: zarith.
-Hint Extern 10 (_ > _) => abstract omega: zarith.
-
-Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
-Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
-Hint Extern 10 (~ _ < _) => abstract omega: zarith.
-Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
-Hint Extern 10 (~ _ > _) => abstract omega: zarith.
-
-Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
-Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
-
-Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
-
-Hint Extern 10 False => abstract omega: zarith.
diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v
deleted file mode 100644
index d2378569fc..0000000000
--- a/plugins/omega/OmegaLemmas.v
+++ /dev/null
@@ -1,307 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Require Import BinInt Znat.
-Local Open Scope Z_scope.
-
-(** Factorization lemmas *)
-
-Theorem Zred_factor0 n : n = n * 1.
-Proof.
-  now Z.nzsimpl.
-Qed.
-
-Theorem Zred_factor1 n : n + n = n * 2.
-Proof.
-  rewrite Z.mul_comm. apply Z.add_diag.
-Qed.
-
-Theorem Zred_factor2 n m : n + n * m = n * (1 + m).
-Proof.
-  rewrite Z.mul_add_distr_l; now Z.nzsimpl.
-Qed.
-
-Theorem Zred_factor3 n m : n * m + n = n * (1 + m).
-Proof.
-  now Z.nzsimpl.
-Qed.
-
-Theorem Zred_factor4 n m p : n * m + n * p = n * (m + p).
-Proof.
-  symmetry; apply Z.mul_add_distr_l.
-Qed.
-
-Theorem Zred_factor5 n m : n * 0 + m = m.
-Proof.
-  now Z.nzsimpl.
-Qed.
-
-Theorem Zred_factor6 n : n = n + 0.
-Proof.
-  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.
-Proof.
-intros x; now exists x.
-Qed.
-
-Lemma OMEGA1 x y : x = y -> 0 <= x -> 0 <= y.
-Proof.
-now intros ->.
-Qed.
-
-Lemma OMEGA2 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
-Proof.
-Z.order_pos.
-Qed.
-
-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 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 x y z : x = 0 -> y = 0 -> x + y * z = 0.
-Proof.
-now intros -> ->.
-Qed.
-
-Lemma OMEGA6 x y z : 0 <= x -> y = 0 -> 0 <= x + y * z.
-Proof.
-intros H ->. now Z.nzsimpl.
-Qed.
-
-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 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 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 v c1 c2 l1 l2 k1 k2 :
- (v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
- v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
-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 v1 c1 l1 l2 k1 :
- (v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
-Proof.
-rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc.
-now rewrite Z.add_assoc.
-Qed.
-
-Lemma OMEGA12 v2 c2 l1 l2 k2 :
- l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
-Proof.
-rewrite ?Z.mul_add_distr_r, ?Z.mul_add_distr_l, ?Z.mul_assoc.
-apply Z.add_shuffle3.
-Qed.
-
-Lemma OMEGA13 (v l1 l2 : Z) (x : positive) :
- v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2.
-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 (v l1 l2 : Z) (x : positive) :
- v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
-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 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 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 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 x y k : x = y * k -> Zne x 0 -> Zne y 0.
-Proof.
- unfold Zne, not. intros. subst; auto.
-Qed.
-
-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 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 (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 (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 (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))) :=
-  eq_ind_r P H (OMEGA10 v c1 c2 l1 l2 k1 k2).
-
-Definition fast_OMEGA11 (v1 c1 l1 l2 k1 : Z) (P : Z -> Prop)
-  (H : P (v1 * (c1 * k1) + (l1 * k1 + l2))) :=
-  eq_ind_r P H (OMEGA11 v1 c1 l1 l2 k1).
-Definition fast_OMEGA12 (v2 c2 l1 l2 k2 : Z) (P : Z -> Prop)
-  (H : P (v2 * (c2 * k2) + (l1 + l2 * k2))) :=
-  eq_ind_r P H (OMEGA12 v2 c2 l1 l2 k2).
-
-Definition fast_OMEGA15 (v c1 c2 l1 l2 k2 : Z) (P : Z -> Prop)
-  (H : P (v * (c1 + c2 * k2) + (l1 + l2 * k2))) :=
-  eq_ind_r P H (OMEGA15 v c1 c2 l1 l2 k2).
-Definition fast_OMEGA16 (v c l k : Z) (P : Z -> Prop)
-  (H : P (v * (c * k) + l * k)) := eq_ind_r P H (OMEGA16 v c l k).
-
-Definition fast_OMEGA13 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
-  (H : P (l1 + l2)) := eq_ind_r P H (OMEGA13 v l1 l2 x).
-
-Definition fast_OMEGA14 (v l1 l2 : Z) (x : positive) (P : Z -> Prop)
-  (H : P (l1 + l2)) := eq_ind_r P H (OMEGA14 v l1 l2 x).
-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 (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 (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 (Z.opp_add_distr x y).
-
-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 (Z.mul_add_distr_r n m p).
-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).
-
-Definition fast_Zred_factor1 (x : Z) (P : Z -> Prop)
-  (H : P (x * 2)) := eq_ind_r P H (Zred_factor1 x).
-
-Definition fast_Zred_factor2 (x y : Z) (P : Z -> Prop)
-  (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor2 x y).
-
-Definition fast_Zred_factor3 (x y : Z) (P : Z -> Prop)
-  (H : P (x * (1 + y))) := eq_ind_r P H (Zred_factor3 x y).
-
-Definition fast_Zred_factor4 (x y z : Z) (P : Z -> Prop)
-  (H : P (x * (y + z))) := eq_ind_r P H (Zred_factor4 x y z).
-
-Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop)
-  (H : P y) := eq_ind_r P H (Zred_factor5 x y).
-
-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.
-Proof.
-  intros n; exists (Z.of_nat n); split; trivial.
-  rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg.
-Qed.
-
-Register fast_Zplus_assoc_reverse as plugins.omega.fast_Zplus_assoc_reverse.
-Register fast_Zplus_assoc as plugins.omega.fast_Zplus_assoc.
-Register fast_Zmult_assoc_reverse as plugins.omega.fast_Zmult_assoc_reverse.
-Register fast_Zplus_permute as plugins.omega.fast_Zplus_permute.
-Register fast_Zplus_comm as plugins.omega.fast_Zplus_comm.
-Register fast_Zmult_comm as plugins.omega.fast_Zmult_comm.
-
-Register OMEGA1 as plugins.omega.OMEGA1.
-Register OMEGA2 as plugins.omega.OMEGA2.
-Register OMEGA3 as plugins.omega.OMEGA3.
-Register OMEGA4 as plugins.omega.OMEGA4.
-Register OMEGA5 as plugins.omega.OMEGA5.
-Register OMEGA6 as plugins.omega.OMEGA6.
-Register OMEGA7 as plugins.omega.OMEGA7.
-Register OMEGA8 as plugins.omega.OMEGA8.
-Register OMEGA9 as plugins.omega.OMEGA9.
-Register fast_OMEGA10 as plugins.omega.fast_OMEGA10.
-Register fast_OMEGA11 as plugins.omega.fast_OMEGA11.
-Register fast_OMEGA12 as plugins.omega.fast_OMEGA12.
-Register fast_OMEGA13 as plugins.omega.fast_OMEGA13.
-Register fast_OMEGA14 as plugins.omega.fast_OMEGA14.
-Register fast_OMEGA15 as plugins.omega.fast_OMEGA15.
-Register fast_OMEGA16 as plugins.omega.fast_OMEGA16.
-Register OMEGA17 as plugins.omega.OMEGA17.
-Register OMEGA18 as plugins.omega.OMEGA18.
-Register OMEGA19 as plugins.omega.OMEGA19.
-Register OMEGA20 as plugins.omega.OMEGA20.
-
-Register fast_Zred_factor0 as plugins.omega.fast_Zred_factor0.
-Register fast_Zred_factor1 as plugins.omega.fast_Zred_factor1.
-Register fast_Zred_factor2 as plugins.omega.fast_Zred_factor2.
-Register fast_Zred_factor3 as plugins.omega.fast_Zred_factor3.
-Register fast_Zred_factor4 as plugins.omega.fast_Zred_factor4.
-Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5.
-Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6.
-
-Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l.
-Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr.
-Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r.
-Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1.
-
-Register new_var as plugins.omega.new_var.
-Register intro_Z as plugins.omega.intro_Z.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
deleted file mode 100644
index 303eb0527a..0000000000
--- a/plugins/omega/OmegaPlugin.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* To strictly import the omega tactic *)
-
-Require ZArith_base.
-Require OmegaLemmas.
-Require PreOmega.
-
-Declare ML Module "omega_plugin".
diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v
deleted file mode 100644
index 303eb0527a..0000000000
--- a/plugins/omega/OmegaTactic.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* To strictly import the omega tactic *)
-
-Require ZArith_base.
-Require OmegaLemmas.
-Require PreOmega.
-
-Declare ML Module "omega_plugin".
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
deleted file mode 100644
index 34533670f8..0000000000
--- a/plugins/omega/PreOmega.v
+++ /dev/null
@@ -1,588 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Require Import Arith Max Min BinInt BinNat Znat Nnat.
-
-Local Open Scope Z_scope.
-
-(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *)
-
-(** These tactic use the complete specification of [Z.div] and
-    [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these
-    functions from the goal without losing information.  The
-    [Z.euclidean_division_equations_cleanup] tactic removes needless
-    hypotheses, which makes tactics like [nia] run faster.  The tactic
-    [Z.to_euclidean_division_equations] combines the handling of both variants
-    of division/quotient and modulo/remainder. *)
-
-Module Z.
-  Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
-  Proof. intro; subst; destruct x; reflexivity. Qed.
-  Lemma div_0_r_ext x y : y = 0 -> x / y = 0.
-  Proof. intro; subst; destruct x; reflexivity. Qed.
-
-  Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x.
-  Proof. intro; subst; destruct x; reflexivity. Qed.
-  Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0.
-  Proof. intro; subst; destruct x; reflexivity. Qed.
-
-  Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y.
-  Proof. intros; apply Z.rem_bound_pos; assumption. Qed.
-  Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y.
-  Proof. rewrite <- Z.rem_opp_r'; intros; apply Z.rem_bound_pos; rewrite ?Z.opp_pos_neg; assumption. Qed.
-  Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0.
-  Proof. rewrite <- (Z.opp_involutive x), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg; apply rem_bound_pos_pos. Qed.
-  Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0.
-  Proof. rewrite <- (Z.opp_involutive x), <- (Z.opp_involutive y), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg, Z.opp_involutive; apply rem_bound_neg_pos. Qed.
-
-  Ltac div_mod_to_equations_generalize x y :=
-    pose proof (Z.div_mod x y);
-    pose proof (Z.mod_pos_bound x y);
-    pose proof (Z.mod_neg_bound x y);
-    pose proof (div_0_r_ext x y);
-    pose proof (mod_0_r_ext x y);
-    let q := fresh "q" in
-    let r := fresh "r" in
-    set (q := x / y) in *;
-    set (r := x mod y) in *;
-    clearbody q r.
-  Ltac quot_rem_to_equations_generalize x y :=
-    pose proof (Z.quot_rem' x y);
-    pose proof (rem_bound_pos_pos x y);
-    pose proof (rem_bound_pos_neg x y);
-    pose proof (rem_bound_neg_pos x y);
-    pose proof (rem_bound_neg_neg x y);
-    pose proof (quot_0_r_ext x y);
-    pose proof (rem_0_r_ext x y);
-    let q := fresh "q" in
-    let r := fresh "r" in
-    set (q := Z.quot x y) in *;
-    set (r := Z.rem x y) in *;
-    clearbody q r.
-
-  Ltac div_mod_to_equations_step :=
-    match goal with
-    | [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y
-    | [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y
-    | [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y
-    | [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y
-    end.
-  Ltac quot_rem_to_equations_step :=
-    match goal with
-    | [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y
-    | [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y
-    | [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
-    | [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
-    end.
-  Ltac div_mod_to_equations' := repeat div_mod_to_equations_step.
-  Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step.
-  Ltac euclidean_division_equations_cleanup :=
-    repeat match goal with
-           | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
-           | [ H : ?x <> ?x -> _ |- _ ] => clear H
-           | [ H : ?x < ?x -> _ |- _ ] => clear H
-           | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
-           | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
-           | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
-           | [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl)
-           | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H
-           | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H
-           | [ H : ?A -> ?B -> _, H' : ?B |- _ ] => specialize (fun a => H a H')
-           | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H
-           | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H
-           | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
-           | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
-           | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
-           | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
-           | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
-           | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
-           | [ H : 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf)))
-           | [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf)))
-           | [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf))
-           | [ H : ?A -> ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf))
-           | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
-           | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
-           | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
-           | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
-           | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
-           | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
-           | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
-           | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
-           end.
-  Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup.
-  Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup.
-  Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup.
-End Z.
-
-Set Warnings "-deprecated-tactic".
-
-(** * zify: the Z-ification tactic *)
-
-(* This tactic searches for nat and N and positive elements in the goal and
-   translates everything into Z. It is meant as a pre-processor for
-   (r)omega; for instance a positivity hypothesis is added whenever
-     - a multiplication is encountered
-     - an atom is encountered (that is a variable or an unknown construct)
-
-   Recognized relations (can be handled as deeply as allowed by setoid rewrite):
-     - { eq, le, lt, ge, gt } on { Z, positive, N, nat }
-
-   Recognized operations:
-     - 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.pred N.succ N.min N.max N.of_nat Z.abs_N
-*)
-
-
-
-
-(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *)
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_unop_core t thm a :=
- (* Let's introduce the specification theorem for t *)
- pose proof (thm a);
- (* Then we replace (t a) everywhere with a fresh variable *)
- let z := fresh "z" in set (z:=t a) in *; clearbody z.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_unop_var_or_term t thm a :=
- (* If a is a variable, no need for aliasing *)
- let za := fresh "z" in
- (rename a into za; rename za into a; zify_unop_core t thm a) ||
- (* Otherwise, a is a complex term: we alias it. *)
- (remember a as za; zify_unop_core t thm za).
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_unop t thm a :=
- (* If a is a scalar, we can simply reduce the unop. *)
- (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *)
- let isz := isZcst a in
- match isz with
-  | true =>
-    let u := eval compute in (t a) in
-    change (t a) with u in *
-  | _ => zify_unop_var_or_term t thm a
- end.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_unop_nored t thm a :=
- (* 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
-  | _ => zify_unop_var_or_term t thm a
- end.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_binop t thm a b:=
- (* works as zify_unop, except that we should be careful when
-    dealing with b, since it can be equal to a *)
- let isza := isZcst a in
- match isza with
-   | true => zify_unop (t a) (thm a) b
-   | _ =>
-       let za := fresh "z" in
-       (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) ||
-       (remember a as za; match goal with
-         | H : za = b |- _ => zify_unop_nored (t za) (thm za) za
-         | _ => zify_unop_nored (t za) (thm za) b
-        end)
- end.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_op_1 :=
-  match goal with
-   | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
-   | |- 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.
-
-
-(** II) Conversion from nat to Z *)
-
-
-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;
-  unfold z in *; clear z.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_nat_rel :=
- match goal with
-  (* I: equalities *)
-  | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
-  | |- (@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 : 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 : 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 : 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 : 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 (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 ] |- _ => change (Z.of_nat O) with Z0 in H
-  | |- context [ Z.of_nat O ] => change (Z.of_nat O) with Z0
-
-  (* S -> number or Z.succ *)
-  | H : context [ Z.of_nat (S ?a) ] |- _ =>
-     let isnat := isnatcst a in
-     match isnat with
-      | true =>
-        let t := eval compute in (Z.of_nat (S a)) in
-        change (Z.of_nat (S a)) with t in H
-      | _ => rewrite (Nat2Z.inj_succ a) in H
-      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
-                hide [Z.of_nat (S a)] in this one hypothesis *)
-        change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
-     end
-  | |- context [ Z.of_nat (S ?a) ] =>
-     let isnat := isnatcst a in
-     match isnat with
-      | true =>
-        let t := eval compute in (Z.of_nat (S a)) in
-        change (Z.of_nat (S a)) with t
-      | _ => rewrite (Nat2Z.inj_succ a)
-      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
-                hide [Z.of_nat (S a)] in the goal *)
-        change (Z.of_nat (S a)) with (Z_of_nat' (S 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 (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.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_nat := repeat zify_nat_rel; repeat zify_nat_op; unfold Z_of_nat' in *.
-
-(* III) conversion from positive to Z *)
-
-Definition Zpos' := Zpos.
-Definition Zneg' := Zneg.
-
-Ltac hide_Zpos t :=
-  let z := fresh "z" in set (z:=Zpos t) in *;
-  change Zpos with Zpos' in z;
-  unfold z in *; clear z.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_positive_rel :=
- match goal with
-  (* I: equalities *)
-  | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
-  | |- (@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)
-  (* III: less or equal *)
-  | 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)
-  (* IV: greater 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)
-  (* V: greater or equal *)
-  | 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)
- end.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_positive_op :=
- match goal with
- (* Z.pow_pos -> Z.pow *)
- | H : context [ Z.pow_pos ?a ?b ] |- _ => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) in H
- | |- context [ Z.pow_pos ?a ?b ]  => change (Z.pow_pos a b) with (Z.pow a (Z.pos b))
- (* Zneg -> -Zpos (except for numbers) *)
-  | H : context [ Zneg ?a ] |- _ =>
-     let isp := isPcst a in
-     match isp with
-      | true => change (Zneg a) with (Zneg' a) in H
-      | _ => change (Zneg a) with (- Zpos a) in H
-     end
-  | |- context [ Zneg ?a ] =>
-     let isp := isPcst a in
-     match isp with
-      | true => change (Zneg a) with (Zneg' a)
-      | _ => change (Zneg a) with (- Zpos a)
-     end
-
-  (* misc type conversions: nat to positive *)
-  | 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)
-
-  (* Z.power_pos *)
-  | 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)
-
-  (* 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)
-
-  (* 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)
-
-  (* 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)
-
-  (* Pos.sub -> Z.max 1 (Z.sub ... ...) *)
-  | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub_max a b) in H
-  | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub_max a b)
-
-  (* 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)
-
-  (* 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)
-
-  (* 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 (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 (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 (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 (Pos2Z.inj_xI a)
-     end
-
-  (* xI : nothing to do, just prevent adding a useless positivity condition *)
-  | H : context [ Zpos xH ] |- _ => hide_Zpos xH
-  | |- context [ Zpos xH ] => hide_Zpos xH
-
-  (* atoms of type positive : we add a positivity condition (if not already there) *)
-  | _ : 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.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_positive :=
- repeat zify_positive_rel; repeat zify_positive_op; unfold Zpos',Zneg' in *.
-
-
-
-
-
-(* IV) conversion from N to Z *)
-
-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;
-  unfold z in *; clear z.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_N_rel :=
- match goal with
-  (* I: equalities *)
-  | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
-  | |- (@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 : 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 : 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 : 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 : context [ (?a >= ?b)%N ] |- _ => rewrite (N2Z.inj_ge a b) in H
-  | |- context [ (?a >= ?b)%N ] =>       rewrite (N2Z.inj_ge a b)
- end.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_N_op :=
- match goal with
-  (* misc type conversions: nat to positive *)
-  | 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)
-
-  (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *)
-  | H : context [ Z.of_N (N.pred ?a) ] |- _ => rewrite (N.pred_sub a) in H
-  | |- context [ Z.of_N (N.pred ?a) ] => rewrite (N.pred_sub a)
-
-  (* 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 *
-
-  (* N.div -> Z.div and a positivity hypothesis *)
-  | H : context [ Z.of_N (N.div ?a ?b) ] |- _ =>
-        pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
-  | |- context [ Z.of_N  (N.div ?a ?b) ] =>
-        pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
-
-  (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *)
-  | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ =>
-    pose proof (N2Z.is_nonneg (N.modulo a b));
-    pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
-    pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
-    rewrite (N2Z.inj_rem a b) in *
-  | |- context [ Z.of_N  (N.div ?a ?b) ] =>
-    pose proof (N2Z.is_nonneg (N.modulo a b));
-    pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
-    pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
-    rewrite (N2Z.inj_rem 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 (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.
-
-#[deprecated( note = "Use 'zify' instead")]
-Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
-
-(** The complete Z-ification tactic *)
-
-Require  Import ZifyClasses ZifyInst.
-Require  Zify.
-
-(* [elim_let] replaces a let binding (x := e : t)
-   by an equation (x = e) if t is an injected type *)
-
-Ltac elim_binding x t ty :=
-  let h := fresh "heq_" x in
-  pose proof (@eq_refl ty x : @eq ty x t) as h;
-  try clearbody x.
-
-Ltac elim_let := zify_iter_let elim_binding.
-
-Ltac zify :=
-  intros ; elim_let ;
-  Zify.zify  ; ZifyInst.zify_saturate.