From 0219dc26914219765300bf2eae792bed49b73562 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 9 Jul 2018 12:57:39 -0400
Subject: Add Z.div_mod_to_quot_rem tactic, put it in zify

The various (micr)omega tactics now support `Z.div` and `Z.modulo`.

I briefly looked into supporting `Nat.div` and `Nat.modulo`, but the
conversions between `Z.div` and `Nat.div` are defined in `ZArith.Zdiv`,
which depends on `Omega`, which depends on `PreOmega`, which is where
`zify` is defined.
---
 CHANGES.md                        |   5 +
 doc/sphinx/addendum/micromega.rst |   4 +-
 plugins/omega/PreOmega.v          |  34 +++-
 test-suite/success/Nia.v          | 325 ++++++++++++++++++++++++++++++++++++++
 4 files changed, 366 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/success/Nia.v

diff --git a/CHANGES.md b/CHANGES.md
index bcdb951a94..6d76c857c9 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -288,6 +288,11 @@ Standard Library
   impacts users running Coq without the init library (`-nois` or
   `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
 
+- Tactic `zify` (and therefore `lia`, `nia`, `romega`, etc) now
+  supports `Z.div` and `Z.modulo` via the `Z.div_mod_to_quot_rem`
+  tactic in `PreOmega.v`, which poses the specifying equation for
+  `Z.div` and `Z.modulo` before replacing them with atoms.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index e799677c59..1aa4a23b5c 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -145,7 +145,7 @@ weakness, the :tacn:`lia` tactic is using recursively a combination of:
 + linear *positivstellensatz* refutations;
 + cutting plane proofs;
 + case split.
-  
+
 Cutting plane proofs
 ~~~~~~~~~~~~~~~~~~~~~~
 
@@ -250,6 +250,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
 .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
+.. [#] Support for :g:`Z.div` and :g:`Z.modulo` is obtained by pre-processing the goal with
+  the `Z.div_mod_to_quot_rem` tactic, which is called by `zify`.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 94a3d40441..387f258bdd 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -12,6 +12,38 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat.
 
 Local Open Scope Z_scope.
 
+(** * [Z.div_mod_to_quot_rem]: the tactic for preprocessing [Z.div] and [Z.modulo] *)
+
+(** This tactic uses the complete specification of [Z.div] and
+    [Z.modulo] to remove these functions from the goal without losing
+    information. *)
+
+Module Z.
+  Lemma div_mod_cases x y
+  : ((x = y * (x/y) + x mod y /\ (0 <= x mod y < y \/ y < x mod y <= 0))
+     \/ (y = 0 /\ x / y = 0 /\ x mod y = 0)).
+  Proof.
+    destruct (Z.eq_dec y 0); subst;
+      [ right | left; auto using Z.div_mod, Z.mod_bound_or ].
+    destruct x; cbv; repeat esplit.
+  Qed.
+
+  Ltac div_mod_to_quot_rem_generalize x y :=
+    pose proof (div_mod_cases 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 div_mod_to_quot_rem_step :=
+    match goal with
+    | [ |- context[?x / ?y] ] => div_mod_to_quot_rem_generalize x y
+    | [ |- context[?x mod ?y] ] => div_mod_to_quot_rem_generalize x y
+    | [ H : context[?x / ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
+    | [ H : context[?x mod ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
+    end.
+  Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step.
+End Z.
 
 (** * zify: the Z-ification tactic *)
 
@@ -423,4 +455,4 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
 
 (** The complete Z-ification tactic *)
 
-Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op.
+Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
new file mode 100644
index 0000000000..da0b2a7a83
--- /dev/null
+++ b/test-suite/success/Nia.v
@@ -0,0 +1,325 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Open Scope Z_scope.
+
+Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
+Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
+
+Ltac unique_pose_proof pf :=
+  let T := type of pf in
+  lazymatch goal with
+  | [ H : T |- _ ] => fail
+  | _ => pose proof pf
+  end.
+
+Ltac saturate_mod_div :=
+  repeat match goal with
+         | [ |- context[?x mod ?y] ] => unique_pose_proof (Z_zerop_or (x / y))
+         | [ H : context[?x mod ?y] |- _ ] => unique_pose_proof (Z_zerop_or (x / y))
+         | [ |- context[?x / ?y] ] => unique_pose_proof (Z_zerop_or y)
+         | [ H : context[?x / ?y] |- _ ] => unique_pose_proof (Z_zerop_or y)
+         end.
+
+Ltac t := intros; saturate_mod_div; try nia.
+
+Ltac destr_step :=
+  match goal with
+  | [ H : and _ _ |- _ ] => destruct H
+  | [ H : or _ _ |- _ ] => destruct H
+  end.
+
+Example mod_0_l: forall x : Z, 0 mod x = 0. Proof. t. Qed.
+Example mod_0_r: forall x : Z, x mod 0 = 0. Proof. intros; nia. Qed.
+Example Z_mod_same_full: forall a : Z, a mod a = 0. Proof. t. Qed.
+Example Zmod_0_l: forall a : Z, 0 mod a = 0. Proof. t. Qed.
+Example Zmod_0_r: forall a : Z, a mod 0 = 0. Proof. intros; nia. Qed.
+Example mod_mod_same: forall x y : Z, (x mod y) mod y = x mod y. Proof. t. Qed.
+Example Zmod_mod: forall a n : Z, (a mod n) mod n = a mod n. Proof. t. Qed.
+Example Zmod_1_r: forall a : Z, a mod 1 = 0. Proof. intros; nia. Qed.
+Example Zmod_div: forall a b : Z, a mod b / b = 0. Proof. intros; nia. Qed.
+Example Z_mod_1_r: forall a : Z, a mod 1 = 0. Proof. intros; nia. Qed.
+Example Z_mod_same: forall a : Z, a > 0 -> a mod a = 0. Proof. t. Qed.
+Example Z_mod_mult: forall a b : Z, (a * b) mod b = 0.
+Proof.
+  intros a b.
+  assert (b = 0 \/ (a * b) / b = a) by nia.
+  nia.
+Qed.
+Example Z_mod_same': forall a : Z, a <> 0 -> a mod a = 0. Proof. t. Qed.
+Example Z_mod_0_l: forall a : Z, a <> 0 -> 0 mod a = 0. Proof. t. Qed.
+Example Zmod_opp_opp: forall a b : Z, - a mod - b = - (a mod b).
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or ((-a)/(-b)) (a/b)).
+  nia.
+Qed.
+Example Z_mod_le: forall a b : Z, 0 <= a -> 0 < b -> a mod b <= a. Proof. t. Qed.
+Example Zmod_le: forall a b : Z, 0 < b -> 0 <= a -> a mod b <= a. Proof. t. Qed.
+Example Zplus_mod_idemp_r: forall a b n : Z, (b + a mod n) mod n = (b + a) mod n.
+Proof. Fail solve [ t ]. Abort.
+Example Zplus_mod_idemp_l: forall a b n : Z, (a mod n + b) mod n = (a + b) mod n. Proof. Fail solve [ t ]. Abort.
+Example Zmult_mod_distr_r: forall a b c : Z, (a * c) mod (b * c) = a mod b * c.
+Proof.
+  intros a b c.
+  destruct (Z_zerop c); try nia.
+  pose proof (Z_eq_dec_or ((a * c) / (b * c)) (a / b)).
+  nia.
+Qed.
+Example Z_mod_zero_opp_full: forall a b : Z, a mod b = 0 -> - a mod b = 0.
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or (a/b) (-(-a/b))).
+  nia.
+Qed.
+Example Zmult_mod_idemp_r: forall a b n : Z, (b * (a mod n)) mod n = (b * a) mod n. Proof. Fail solve [ t ]. Abort.
+Example Zmult_mod_idemp_l: forall a b n : Z, (a mod n * b) mod n = (a * b) mod n. Proof. Fail solve [ t ]. Abort.
+Example Zminus_mod_idemp_r: forall a b n : Z, (a - b mod n) mod n = (a - b) mod n. Proof. Fail solve [ t ]. Abort.
+Example Zminus_mod_idemp_l: forall a b n : Z, (a mod n - b) mod n = (a - b) mod n. Proof. Fail solve [ t ]. Abort.
+Example Z_mod_plus_full: forall a b c : Z, (a + b * c) mod c = a mod c.
+Proof.
+  intros a b c.
+  pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c + b)).
+  nia.
+Qed.
+Example Zmult_mod_distr_l: forall a b c : Z, (c * a) mod (c * b) = c * (a mod b).
+Proof.
+  intros a b c.
+  destruct (Z_zerop c); try nia.
+  pose proof (Z_eq_dec_or ((c * a) / (c * b)) (a / b)).
+  nia.
+Qed.
+Example Z_mod_zero_opp_r: forall a b : Z, a mod b = 0 -> a mod - b = 0.
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or (a/b) (-(a/-b))).
+  nia.
+Qed.
+Example Zmod_1_l: forall a : Z, 1 < a -> 1 mod a = 1. Proof. t. Qed.
+Example Z_mod_1_l: forall a : Z, 1 < a -> 1 mod a = 1. Proof. t. Qed.
+Example Z_mod_mul: forall a b : Z, b <> 0 -> (a * b) mod b = 0.
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or ((a*b)/b) a).
+  nia.
+Qed.
+Example Zminus_mod: forall a b n : Z, (a - b) mod n = (a mod n - b mod n) mod n. Proof. Fail intros; nia. Abort.
+Example Zplus_mod: forall a b n : Z, (a + b) mod n = (a mod n + b mod n) mod n. Proof. Fail intros; nia. Abort.
+Example Zmult_mod: forall a b n : Z, (a * b) mod n = (a mod n * (b mod n)) mod n. Proof. Fail intros; nia. Abort.
+Example Z_mod_mod: forall a n : Z, n <> 0 -> (a mod n) mod n = a mod n. Proof. t. Qed.
+Example Z_mod_div: forall a b : Z, b <> 0 -> a mod b / b = 0. Proof. intros; nia. Qed.
+Example Z_div_exact_full_1: forall a b : Z, a = b * (a / b) -> a mod b = 0. Proof. intros; nia. Qed.
+Example Z_mod_pos_bound: forall a b : Z, 0 < b -> 0 <= a mod b < b. Proof. intros; nia. Qed.
+Example Z_mod_sign_mul: forall a b : Z, b <> 0 -> 0 <= a mod b * b. Proof. intros; nia. Qed.
+Example Z_mod_neg_bound: forall a b : Z, b < 0 -> b < a mod b <= 0. Proof. intros; nia. Qed.
+Example Z_mod_neg: forall a b : Z, b < 0 -> b < a mod b <= 0. Proof. intros; nia. Qed.
+Example div_mod_small: forall x y : Z, 0 <= x < y -> x mod y = x. Proof. t. Qed.
+Example Zmod_small: forall a n : Z, 0 <= a < n -> a mod n = a. Proof. t. Qed.
+Example Z_mod_small: forall a b : Z, 0 <= a < b -> a mod b = a. Proof. t. Qed.
+Example Z_div_zero_opp_full: forall a b : Z, a mod b = 0 -> - a / b = - (a / b). Proof. intros; nia. Qed.
+Example Z_mod_zero_opp: forall a b : Z, b > 0 -> a mod b = 0 -> - a mod b = 0.
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or (a/b) (-(-a/b))).
+  nia.
+Qed.
+Example Z_div_zero_opp_r: forall a b : Z, a mod b = 0 -> a / - b = - (a / b). Proof. intros; nia. Qed.
+Example Z_mod_lt: forall a b : Z, b > 0 -> 0 <= a mod b < b. Proof. intros; nia. Qed.
+Example Z_mod_opp_opp: forall a b : Z, b <> 0 -> - a mod - b = - (a mod b).
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or ((-a)/(-b)) ((a/b))).
+  nia.
+Qed.
+Example Z_mod_bound_pos: forall a b : Z, 0 <= a -> 0 < b -> 0 <= a mod b < b. Proof. intros; nia. Qed.
+Example Z_mod_opp_l_z: forall a b : Z, b <> 0 -> a mod b = 0 -> - a mod b = 0.
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or (a/b) (-(-a/b))).
+  nia.
+Qed.
+Example Z_mod_plus: forall a b c : Z, c > 0 -> (a + b * c) mod c = a mod c.
+Proof.
+  intros a b c.
+  pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c+b)).
+  nia.
+Qed.
+Example Z_mod_opp_r_z: forall a b : Z, b <> 0 -> a mod b = 0 -> a mod - b = 0.
+Proof.
+  intros a b.
+  pose proof (Z_eq_dec_or (a/b) (-(a/-b))).
+  nia.
+Qed.
+Example Zmod_eq: forall a b : Z, b > 0 -> a mod b = a - a / b * b. Proof. intros; nia. Qed.
+Example Z_div_exact_2: forall a b : Z, b > 0 -> a mod b = 0 -> a = b * (a / b). Proof. intros; nia. Qed.
+Example Z_div_mod_eq: forall a b : Z, b > 0 -> a = b * (a / b) + a mod b. Proof. intros; nia. Qed.
+Example Z_div_exact_1: forall a b : Z, b > 0 -> a = b * (a / b) -> a mod b = 0. Proof. intros; nia. Qed.
+Example Z_mod_add: forall a b c : Z, c <> 0 -> (a + b * c) mod c = a mod c.
+Proof.
+  intros a b c.
+  pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c+b)).
+  nia.
+Qed.
+Example Z_mod_nz_opp_r: forall a b : Z, a mod b <> 0 -> a mod - b = a mod b - b.
+Proof.
+  intros a b.
+  assert (a mod b <> 0 -> a / -b = -(a/b)-1) by t.
+  nia.
+Qed.
+Example Z_mul_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n * b) mod n = (a * b) mod n. Proof. Fail intros; nia. Abort.
+Example Z_mod_nz_opp_full: forall a b : Z, a mod b <> 0 -> - a mod b = b - a mod b.
+Proof.
+  intros a b.
+  assert (a mod b <> 0 -> -a/b = -1-a/b) by nia.
+  nia.
+Qed.
+Example Z_add_mod_idemp_r: forall a b n : Z, n <> 0 -> (a + b mod n) mod n = (a + b) mod n. Proof. Fail intros; nia. Abort.
+Example Z_add_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n + b) mod n = (a + b) mod n. Proof. Fail intros; nia. Abort.
+Example Z_mul_mod_idemp_r: forall a b n : Z, n <> 0 -> (a * (b mod n)) mod n = (a * b) mod n. Proof. Fail intros; nia. Abort.
+Example Zmod_eq_full: forall a b : Z, b <> 0 -> a mod b = a - a / b * b. Proof. intros; nia. Qed.
+Example div_eq: forall x y : Z, y <> 0 -> x mod y = 0 -> x / y * y = x. Proof. intros; nia. Qed.
+Example Z_mod_eq: forall a b : Z, b <> 0 -> a mod b = a - b * (a / b). Proof. intros; nia. Qed.
+Example Z_mod_sign_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> Z.sgn (a mod b) = Z.sgn b. Proof. intros; nia. Qed.
+Example Z_div_exact_full_2: forall a b : Z, b <> 0 -> a mod b = 0 -> a = b * (a / b). Proof. intros; nia. Qed.
+Example Z_div_mod: forall a b : Z, b <> 0 -> a = b * (a / b) + a mod b. Proof. intros; nia. Qed.
+Example Z_add_mod: forall a b n : Z, n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n. Proof. Fail intros; nia. Abort.
+Example Z_mul_mod: forall a b n : Z, n <> 0 -> (a * b) mod n = (a mod n * (b mod n)) mod n. Proof. Fail intros; nia. Abort.
+Example Z_div_exact: forall a b : Z, b <> 0 -> a = b * (a / b) <-> a mod b = 0. Proof. intros; nia. Qed.
+Example Z_div_opp_l_z: forall a b : Z, b <> 0 -> a mod b = 0 -> - a / b = - (a / b). Proof. intros; nia. Qed.
+Example Z_div_opp_r_z: forall a b : Z, b <> 0 -> a mod b = 0 -> a / - b = - (a / b). Proof. intros; nia. Qed.
+Example Z_mod_opp_r_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> a mod - b = a mod b - b.
+Proof.
+  intros a b.
+  assert (a mod b <> 0 -> a/(-b) = -1-a/b) by nia.
+  nia.
+Qed.
+Example Z_mul_mod_distr_r: forall a b c : Z, b <> 0 -> c <> 0 -> (a * c) mod (b * c) = a mod b * c.
+Proof.
+  intros a b c.
+  pose proof (Z_eq_dec_or ((a*c)/(b*c)) (a/b)).
+  nia.
+Qed.
+Example Z_mul_mod_distr_l: forall a b c : Z, b <> 0 -> c <> 0 -> (c * a) mod (c * b) = c * (a mod b).
+Proof.
+  intros a b c.
+  pose proof (Z_eq_dec_or ((c*a)/(c*b)) (a/b)).
+  nia.
+Qed.
+Example Z_mod_opp_l_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> - a mod b = b - a mod b.
+Proof.
+  intros a b.
+  assert (a mod b <> 0 -> -a/b = -1-a/b) by nia.
+  nia.
+Qed.
+Example mod_eq: forall x x' y : Z, x / y = x' / y -> x mod y = x' mod y -> y <> 0 -> x = x'. Proof. intros; nia. Qed.
+Example Z_div_nz_opp_r: forall a b : Z, a mod b <> 0 -> a / - b = - (a / b) - 1. Proof. intros; nia. Qed.
+Example Z_div_nz_opp_full: forall a b : Z, a mod b <> 0 -> - a / b = - (a / b) - 1. Proof. intros; nia. Qed.
+Example Zmod_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> r = a mod b.
+Proof.
+  intros a b q r ??.
+  assert (q = a / b) by nia.
+  nia.
+Qed.
+Example Z_mod_unique_neg: forall a b q r : Z, b < r <= 0 -> a = b * q + r -> r = a mod b.
+Proof.
+  intros a b q r ??.
+  assert (q = a / b) by nia.
+  nia.
+Qed.
+Example Z_mod_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> r = a mod b.
+Proof.
+  intros a b q r ??.
+  assert (q = a / b) by nia.
+  nia.
+Qed.
+Example Z_rem_mul_r: forall a b c : Z, b <> 0 -> 0 < c -> a mod (b * c) = a mod b + b * ((a / b) mod c).
+Proof.
+  intros a b c ??.
+  assert (a / (b * c) = ((a / b) / c)) by nia.
+  nia.
+Qed.
+Example Z_mod_bound_or: forall a b : Z, b <> 0 -> 0 <= a mod b < b \/ b < a mod b <= 0. Proof. intros; nia. Qed.
+Example Z_div_opp_l_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> - a / b = - (a / b) - 1. Proof. intros; nia. Qed.
+Example Z_div_opp_r_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> a / - b = - (a / b) - 1. Proof. intros; nia. Qed.
+Example Z_mod_small_iff: forall a b : Z, b <> 0 -> a mod b = a <-> 0 <= a < b \/ b < a <= 0. Proof. t. Qed.
+Example Z_mod_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> r = a mod b.
+Proof.
+  intros a b q r ??.
+  assert (q = a/b) by nia.
+  nia.
+Qed.
+Example Z_opp_mod_bound_or: forall a b : Z, b <> 0 -> 0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0. Proof. intros; nia. Qed.
+
+Example Zdiv_0_r: forall a : Z, a / 0 = 0. Proof. intros; nia. Qed.
+Example Zdiv_0_l: forall a : Z, 0 / a = 0. Proof. intros; nia. Qed.
+Example Z_div_1_r: forall a : Z, a / 1 = a. Proof. intros; nia. Qed.
+Example Zdiv_1_r: forall a : Z, a / 1 = a. Proof. intros; nia. Qed.
+Example Zdiv_opp_opp: forall a b : Z, - a / - b = a / b. Proof. intros; nia. Qed.
+Example Z_div_0_l: forall a : Z, a <> 0 -> 0 / a = 0. Proof. intros; nia. Qed.
+Example Z_div_pos: forall a b : Z, b > 0 -> 0 <= a -> 0 <= a / b. Proof. intros; nia. Qed.
+Example Z_div_ge0: forall a b : Z, b > 0 -> a >= 0 -> a / b >= 0. Proof. intros; nia. Qed.
+Example Z_div_pos': forall a b : Z, 0 <= a -> 0 < b -> 0 <= a / b. Proof. intros; nia. Qed.
+Example Z_mult_div_ge: forall a b : Z, b > 0 -> b * (a / b) <= a. Proof. intros; nia. Qed.
+Example Z_mult_div_ge_neg: forall a b : Z, b < 0 -> b * (a / b) >= a. Proof. intros; nia. Qed.
+Example Z_mul_div_le: forall a b : Z, 0 < b -> b * (a / b) <= a. Proof. intros; nia. Qed.
+Example Z_mul_div_ge: forall a b : Z, b < 0 -> a <= b * (a / b). Proof. intros; nia. Qed.
+Example Z_div_same: forall a : Z, a > 0 -> a / a = 1. Proof. intros; nia. Qed.
+Example Z_div_mult: forall a b : Z, b > 0 -> a * b / b = a. Proof. intros; nia. Qed.
+Example Z_mul_succ_div_gt: forall a b : Z, 0 < b -> a < b * Z.succ (a / b). Proof. intros; nia. Qed.
+Example Z_mul_succ_div_lt: forall a b : Z, b < 0 -> b * Z.succ (a / b) < a. Proof. intros; nia. Qed.
+Example Zdiv_1_l: forall a : Z, 1 < a -> 1 / a = 0. Proof. intros; nia. Qed.
+Example Z_div_1_l: forall a : Z, 1 < a -> 1 / a = 0. Proof. intros; nia. Qed.
+Example Z_div_str_pos: forall a b : Z, 0 < b <= a -> 0 < a / b. Proof. intros; nia. Qed.
+Example Z_div_ge: forall a b c : Z, c > 0 -> a >= b -> a / c >= b / c. Proof. intros; nia. Qed.
+Example Z_div_mult_full: forall a b : Z, b <> 0 -> a * b / b = a. Proof. intros; nia. Qed.
+Example Z_div_same': forall a : Z, a <> 0 -> a / a = 1. Proof. intros; nia. Qed.
+Example Zdiv_lt_upper_bound: forall a b q : Z, 0 < b -> a < q * b -> a / b < q. Proof. intros; nia. Qed.
+Example Z_div_mul: forall a b : Z, b <> 0 -> a * b / b = a. Proof. intros; nia. Qed.
+Example Z_div_lt: forall a b : Z, 0 < a -> 1 < b -> a / b < a. Proof. intros; nia. Qed.
+Example Z_div_le_mono: forall a b c : Z, 0 < c -> a <= b -> a / c <= b / c. Proof. intros; nia. Qed.
+Example Zdiv_sgn: forall a b : Z, 0 <= Z.sgn (a / b) * Z.sgn a * Z.sgn b. Proof. intros; nia. Qed.
+Example Z_div_same_full: forall a : Z, a <> 0 -> a / a = 1. Proof. intros; nia. Qed.
+Example Z_div_lt_upper_bound: forall a b q : Z, 0 < b -> a < b * q -> a / b < q. Proof. intros; nia. Qed.
+Example Z_div_le: forall a b c : Z, c > 0 -> a <= b -> a / c <= b / c. Proof. intros; nia. Qed.
+Example Z_div_le_lower_bound: forall a b q : Z, 0 < b -> b * q <= a -> q <= a / b. Proof. intros; nia. Qed.
+Example Zdiv_le_lower_bound: forall a b q : Z, 0 < b -> q * b <= a -> q <= a / b. Proof. intros; nia. Qed.
+Example Zdiv_le_upper_bound: forall a b q : Z, 0 < b -> a <= q * b -> a / b <= q. Proof. intros; nia. Qed.
+Example Z_div_le_upper_bound: forall a b q : Z, 0 < b -> a <= b * q -> a / b <= q. Proof. intros; nia. Qed.
+Example Z_div_small: forall a b : Z, 0 <= a < b -> a / b = 0. Proof. intros; nia. Qed.
+Example Zdiv_small: forall a b : Z, 0 <= a < b -> a / b = 0. Proof. intros; nia. Qed.
+Example Z_div_opp_opp: forall a b : Z, b <> 0 -> - a / - b = a / b. Proof. intros; nia. Qed.
+Example Zdiv_mult_cancel_r: forall a b c : Z, c <> 0 -> a * c / (b * c) = a / b. Proof. intros; nia. Qed.
+Example Z_div_unique_exact: forall a b q : Z, b <> 0 -> a = b * q -> q = a / b. Proof. intros; nia. Qed.
+Example Zdiv_mult_cancel_l: forall a b c : Z, c <> 0 -> c * a / (c * b) = a / b. Proof. intros; nia. Qed.
+Example Zdiv_le_compat_l: forall p q r : Z, 0 <= p -> 0 < q < r -> p / r <= p / q.
+Proof.
+  intros p q r ??.
+  assert (p mod r <= p mod q \/ p mod q <= p mod r) by nia.
+  assert (0 <= p / r) by nia.
+  assert (0 <= p / q) by nia.
+  nia.
+Qed.
+Example Z_div_le_compat_l: forall p q r : Z, 0 <= p -> 0 < q <= r -> p / r <= p / q.
+Proof.
+  intros p q r ??.
+  assert (p mod r <= p mod q \/ p mod q <= p mod r) by nia.
+  assert (0 <= p / r) by nia.
+  assert (0 <= p / q) by nia.
+  nia.
+Qed.
+Example Zdiv_Zdiv: forall a b c : Z, 0 <= b -> 0 <= c -> a / b / c = a / (b * c). Proof. intros; nia. Qed.
+Example Z_div_plus: forall a b c : Z, c > 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed.
+Example Z_div_lt': forall a b : Z, b >= 2 -> a > 0 -> a / b < a. Proof. intros; nia. Qed.
+Example Zdiv_mult_le: forall a b c : Z, 0 <= a -> 0 <= b -> 0 <= c -> c * (a / b) <= c * a / b. Proof. intros; nia. Qed.
+Example Z_div_add_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof. intros; nia. Qed.
+Example Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof. intros; nia. Qed.
+Example Z_div_add: forall a b c : Z, c <> 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed.
+Example Z_div_plus_full: forall a b c : Z, c <> 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed.
+Example Z_div_mul_le: forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b. Proof. intros; nia. Qed.
+Example Z_div_mul_cancel_r: forall a b c : Z, b <> 0 -> c <> 0 -> a * c / (b * c) = a / b. Proof. intros; nia. Qed.
+Example Z_div_div: forall a b c : Z, b <> 0 -> 0 < c -> a / b / c = a / (b * c). Proof. intros; nia. Qed.
+Example Z_div_mul_cancel_l: forall a b c : Z, b <> 0 -> c <> 0 -> c * a / (c * b) = a / b. Proof. intros; nia. Qed.
+Example Z_div_unique_neg: forall a b q r : Z, b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
+Example Zdiv_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
+Example Z_div_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
+Example Z_div_small_iff: forall a b : Z, b <> 0 -> a / b = 0 <-> 0 <= a < b \/ b < a <= 0. Proof. intros; nia. Qed.
+Example Z_div_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
-- 
cgit v1.2.3


From 7bc08910ad7451d5e45102653d33e89aed5ae12b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 16 Jul 2018 20:08:02 -0400
Subject: Don't pose any disjunctions in div_mod_to_quot_rem

Disjunctions seem to have a negative performance impact, so let's try
implications instead.
---
 plugins/omega/PreOmega.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 387f258bdd..1e0922e1ca 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -19,17 +19,17 @@ Local Open Scope Z_scope.
     information. *)
 
 Module Z.
-  Lemma div_mod_cases x y
-  : ((x = y * (x/y) + x mod y /\ (0 <= x mod y < y \/ y < x mod y <= 0))
-     \/ (y = 0 /\ x / y = 0 /\ x mod y = 0)).
-  Proof.
-    destruct (Z.eq_dec y 0); subst;
-      [ right | left; auto using Z.div_mod, Z.mod_bound_or ].
-    destruct x; cbv; repeat esplit.
-  Qed.
+  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.
 
   Ltac div_mod_to_quot_rem_generalize x y :=
-    pose proof (div_mod_cases 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 *;
-- 
cgit v1.2.3


From 0c99020482e96ceb05799c47ffbcaef0e89b4b1f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 3 Dec 2018 16:45:49 -0500
Subject: Don't bundle Z.div_mod_quot_rem into zify

Alas, I have not had time to work on imrpoving the performance of nia,
and there has been a request to include this tactic (which is useful on
its own) without bundling it into `zify`.  So that is what we do here.

I leave the definition of it in `PreOmega` in case we want to eventually
include it in `zify`/`nia`.
---
 doc/sphinx/addendum/micromega.rst | 4 ++--
 plugins/omega/PreOmega.v          | 2 +-
 test-suite/success/Nia.v          | 3 +++
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 1aa4a23b5c..2ace8a59e1 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -250,8 +250,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
 .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
-.. [#] Support for :g:`Z.div` and :g:`Z.modulo` is obtained by pre-processing the goal with
-  the `Z.div_mod_to_quot_rem` tactic, which is called by `zify`.
+.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by pre-processing the goal with
+  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 1e0922e1ca..08bfec84bc 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -455,4 +455,4 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
 
 (** The complete Z-ification tactic *)
 
-Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op.
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index da0b2a7a83..9a13e41e07 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,6 +2,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
+(** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this file *)
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
 
-- 
cgit v1.2.3


From 4e66d30ba33310dfc96f7f1e57c651db9fc53c97 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 3 Dec 2018 18:04:49 -0500
Subject: Remove remainder of `Abort`s in test-suite Nia.v

Note that we define a `cleanup` tactic which is essential for speed of
reasoning.  Perhaps this tactic should make it into the code for
`Z.div_mod_to_quot_rem` somewhere?

```coq
Ltac cleanup :=
  repeat match goal with
         | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
         | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
         | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
         | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
         | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
         | _ => progress subst
         end.
```
---
 test-suite/success/Nia.v | 151 +++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 134 insertions(+), 17 deletions(-)

diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 9a13e41e07..b79a6bde3d 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,8 +2,20 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
-(** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this file *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+Ltac cleanup :=
+  repeat match goal with
+         | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
+         | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
+         | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
+         | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+         | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+         | _ => progress subst
+         end.
+
+(** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
+    file.  Note that we also add a [cleanup] tactic, which is very
+    important for speed purposes. *)
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; cleanup.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
@@ -59,8 +71,23 @@ Qed.
 Example Z_mod_le: forall a b : Z, 0 <= a -> 0 < b -> a mod b <= a. Proof. t. Qed.
 Example Zmod_le: forall a b : Z, 0 < b -> 0 <= a -> a mod b <= a. Proof. t. Qed.
 Example Zplus_mod_idemp_r: forall a b n : Z, (b + a mod n) mod n = (b + a) mod n.
-Proof. Fail solve [ t ]. Abort.
-Example Zplus_mod_idemp_l: forall a b n : Z, (a mod n + b) mod n = (a + b) mod n. Proof. Fail solve [ t ]. Abort.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((b + a mod n) / n = (b / n) + (b mod n + a mod n) / n)
+    by nia.
+  assert ((b + a) / n = (b / n) + (a / n) + (b mod n + a mod n) / n)
+    by nia.
+  nia.
+Qed.
+Example Zplus_mod_idemp_l: forall a b n : Z, (a mod n + b) mod n = (a + b) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((a mod n + b) / n = (b / n) + (b mod n + a mod n) / n) by nia.
+  assert ((a + b) / n = (b / n) + (a / n) + (b mod n + a mod n) / n) by nia.
+  nia.
+Qed.
 Example Zmult_mod_distr_r: forall a b c : Z, (a * c) mod (b * c) = a mod b * c.
 Proof.
   intros a b c.
@@ -74,10 +101,42 @@ Proof.
   pose proof (Z_eq_dec_or (a/b) (-(-a/b))).
   nia.
 Qed.
-Example Zmult_mod_idemp_r: forall a b n : Z, (b * (a mod n)) mod n = (b * a) mod n. Proof. Fail solve [ t ]. Abort.
-Example Zmult_mod_idemp_l: forall a b n : Z, (a mod n * b) mod n = (a * b) mod n. Proof. Fail solve [ t ]. Abort.
-Example Zminus_mod_idemp_r: forall a b n : Z, (a - b mod n) mod n = (a - b) mod n. Proof. Fail solve [ t ]. Abort.
-Example Zminus_mod_idemp_l: forall a b n : Z, (a mod n - b) mod n = (a - b) mod n. Proof. Fail solve [ t ]. Abort.
+Example Zmult_mod_idemp_r: forall a b n : Z, (b * (a mod n)) mod n = (b * a) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((b * (a mod n)) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n)
+    by nia.
+  assert ((b * a) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n)
+    by nia.
+  nia.
+Qed.
+Example Zmult_mod_idemp_l: forall a b n : Z, (a mod n * b) mod n = (a * b) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert (((a mod n) * b) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n)
+    by nia.
+  assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n)
+    by nia.
+  nia.
+Qed.
+Example Zminus_mod_idemp_r: forall a b n : Z, (a - b mod n) mod n = (a - b) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((a - b mod n) / n = a / n + ((a mod n) - (b mod n)) / n) by nia.
+  assert ((a - b) / n = a / n - b / n + ((a mod n) - (b mod n)) / n) by nia.
+  nia.
+Qed.
+Example Zminus_mod_idemp_l: forall a b n : Z, (a mod n - b) mod n = (a - b) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((a mod n - b) / n = - (b / n) + ((a mod n) - (b mod n)) / n) by nia.
+  assert ((a - b) / n = a / n - b / n + ((a mod n) - (b mod n)) / n) by nia.
+  nia.
+Qed.
 Example Z_mod_plus_full: forall a b c : Z, (a + b * c) mod c = a mod c.
 Proof.
   intros a b c.
@@ -105,9 +164,28 @@ Proof.
   pose proof (Z_eq_dec_or ((a*b)/b) a).
   nia.
 Qed.
-Example Zminus_mod: forall a b n : Z, (a - b) mod n = (a mod n - b mod n) mod n. Proof. Fail intros; nia. Abort.
-Example Zplus_mod: forall a b n : Z, (a + b) mod n = (a mod n + b mod n) mod n. Proof. Fail intros; nia. Abort.
-Example Zmult_mod: forall a b n : Z, (a * b) mod n = (a mod n * (b mod n)) mod n. Proof. Fail intros; nia. Abort.
+Example Zminus_mod: forall a b n : Z, (a - b) mod n = (a mod n - b mod n) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((a - b) / n = (a / n) - (b / n) + ((a mod n) - (b mod n)) / n) by nia.
+  nia.
+Qed.
+Example Zplus_mod: forall a b n : Z, (a + b) mod n = (a mod n + b mod n) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((a + b) / n = (a / n) + (b / n) + ((a mod n) + (b mod n)) / n) by nia.
+  nia.
+Qed.
+Example Zmult_mod: forall a b n : Z, (a * b) mod n = (a mod n * (b mod n)) mod n.
+Proof.
+  intros a b n.
+  destruct (Z_zerop n); [ subst; nia | ].
+  assert ((a * b) / n = n * (a / n) * (b / n) + (a mod n) * (b / n) + (a / n) * (b mod n) + ((a mod n) * (b mod n)) / n)
+    by nia.
+  nia.
+Qed.
 Example Z_mod_mod: forall a n : Z, n <> 0 -> (a mod n) mod n = a mod n. Proof. t. Qed.
 Example Z_mod_div: forall a b : Z, b <> 0 -> a mod b / b = 0. Proof. intros; nia. Qed.
 Example Z_div_exact_full_1: forall a b : Z, a = b * (a / b) -> a mod b = 0. Proof. intros; nia. Qed.
@@ -168,24 +246,63 @@ Proof.
   assert (a mod b <> 0 -> a / -b = -(a/b)-1) by t.
   nia.
 Qed.
-Example Z_mul_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n * b) mod n = (a * b) mod n. Proof. Fail intros; nia. Abort.
+Example Z_mul_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n * b) mod n = (a * b) mod n.
+Proof.
+  intros a b n ?.
+  assert (((a mod n) * b) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n)
+    by nia.
+  assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n)
+    by nia.
+  nia.
+Qed.
 Example Z_mod_nz_opp_full: forall a b : Z, a mod b <> 0 -> - a mod b = b - a mod b.
 Proof.
   intros a b.
   assert (a mod b <> 0 -> -a/b = -1-a/b) by nia.
   nia.
 Qed.
-Example Z_add_mod_idemp_r: forall a b n : Z, n <> 0 -> (a + b mod n) mod n = (a + b) mod n. Proof. Fail intros; nia. Abort.
-Example Z_add_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n + b) mod n = (a + b) mod n. Proof. Fail intros; nia. Abort.
-Example Z_mul_mod_idemp_r: forall a b n : Z, n <> 0 -> (a * (b mod n)) mod n = (a * b) mod n. Proof. Fail intros; nia. Abort.
+Example Z_add_mod_idemp_r: forall a b n : Z, n <> 0 -> (a + b mod n) mod n = (a + b) mod n.
+Proof.
+  intros a b n ?.
+  assert ((a + b mod n) / n = (a / n) + (a mod n + b mod n) / n) by nia.
+  assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia.
+  nia.
+Qed.
+Example Z_add_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n + b) mod n = (a + b) mod n.
+Proof.
+  intros a b n ?.
+  assert ((a mod n + b) / n = (b / n) + (a mod n + b mod n) / n) by nia.
+  assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia.
+  nia.
+Qed.
+Example Z_mul_mod_idemp_r: forall a b n : Z, n <> 0 -> (a * (b mod n)) mod n = (a * b) mod n.
+Proof.
+  intros a b n ?.
+  assert ((a * (b mod n)) / n = (a / n) * (b mod n) + ((a mod n) * (b mod n)) / n)
+    by nia.
+  assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((a mod n) * (b mod n)) / n)
+    by nia.
+  nia.
+Qed.
 Example Zmod_eq_full: forall a b : Z, b <> 0 -> a mod b = a - a / b * b. Proof. intros; nia. Qed.
 Example div_eq: forall x y : Z, y <> 0 -> x mod y = 0 -> x / y * y = x. Proof. intros; nia. Qed.
 Example Z_mod_eq: forall a b : Z, b <> 0 -> a mod b = a - b * (a / b). Proof. intros; nia. Qed.
 Example Z_mod_sign_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> Z.sgn (a mod b) = Z.sgn b. Proof. intros; nia. Qed.
 Example Z_div_exact_full_2: forall a b : Z, b <> 0 -> a mod b = 0 -> a = b * (a / b). Proof. intros; nia. Qed.
 Example Z_div_mod: forall a b : Z, b <> 0 -> a = b * (a / b) + a mod b. Proof. intros; nia. Qed.
-Example Z_add_mod: forall a b n : Z, n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n. Proof. Fail intros; nia. Abort.
-Example Z_mul_mod: forall a b n : Z, n <> 0 -> (a * b) mod n = (a mod n * (b mod n)) mod n. Proof. Fail intros; nia. Abort.
+Example Z_add_mod: forall a b n : Z, n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n.
+Proof.
+  intros a b n ?.
+  assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia.
+  nia.
+Qed.
+Example Z_mul_mod: forall a b n : Z, n <> 0 -> (a * b) mod n = (a mod n * (b mod n)) mod n.
+Proof.
+  intros a b n ?.
+  assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((a mod n) * (b mod n)) / n)
+    by nia.
+  nia.
+Qed.
 Example Z_div_exact: forall a b : Z, b <> 0 -> a = b * (a / b) <-> a mod b = 0. Proof. intros; nia. Qed.
 Example Z_div_opp_l_z: forall a b : Z, b <> 0 -> a mod b = 0 -> - a / b = - (a / b). Proof. intros; nia. Qed.
 Example Z_div_opp_r_z: forall a b : Z, b <> 0 -> a mod b = 0 -> a / - b = - (a / b). Proof. intros; nia. Qed.
-- 
cgit v1.2.3


From a10076e834720c05e55397c9e26b9d7a8786298b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 3 Dec 2018 18:10:03 -0500
Subject: Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanup

Also fold it into `Z.div_mod_to_quot_rem`

Note that the test-suite file is a bit slow.  On my machine, it is

```
real    2m32.983s
user    2m32.544s
sys     0m0.492s
```
---
 plugins/omega/PreOmega.v | 14 ++++++++++++--
 test-suite/success/Nia.v | 15 ++-------------
 2 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 08bfec84bc..7ebc2fb04f 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -16,7 +16,8 @@ Local Open Scope Z_scope.
 
 (** This tactic uses the complete specification of [Z.div] and
     [Z.modulo] to remove these functions from the goal without losing
-    information. *)
+    information.  The [Z.div_mod_to_quot_rem_cleanup] tactic removes
+    needless hypotheses, which makes tactics like [nia] run faster. *)
 
 Module Z.
   Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
@@ -42,7 +43,16 @@ Module Z.
     | [ H : context[?x / ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
     | [ H : context[?x mod ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
     end.
-  Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step.
+  Ltac div_mod_to_quot_rem' := repeat div_mod_to_quot_rem_step.
+  Ltac div_mod_to_quot_rem_cleanup :=
+    repeat match goal with
+           | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
+           | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
+           | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
+           | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           end.
+  Ltac div_mod_to_quot_rem := div_mod_to_quot_rem'; div_mod_to_quot_rem_cleanup.
 End Z.
 
 (** * zify: the Z-ification tactic *)
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index b79a6bde3d..6cb645d9eb 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,20 +2,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
-Ltac cleanup :=
-  repeat match goal with
-         | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
-         | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
-         | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
-         | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
-         | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
-         | _ => progress subst
-         end.
-
 (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
-    file.  Note that we also add a [cleanup] tactic, which is very
-    important for speed purposes. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; cleanup.
+    file. *)
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
-- 
cgit v1.2.3


From 20fc76a75c13f61d467834414e97776477ec203c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 3 Dec 2018 18:19:57 -0500
Subject: Add subst to the end of nia in the test-suite

This speeds up the file from 2m32s to

```
real    0m41.851s
user    0m41.512s
sys     0m0.376s
```

Also note the `subst` trick in the doc.
---
 doc/sphinx/addendum/micromega.rst | 3 ++-
 test-suite/success/Nia.v          | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 2ace8a59e1..5f199d28f5 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -251,7 +251,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
 .. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by pre-processing the goal with
-  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.
+  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.  Note that additionally
+  running ``subst`` can speed up things up, sometimees by almost 4x in practice.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 6cb645d9eb..c157173b77 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -4,7 +4,7 @@ Open Scope Z_scope.
 
 (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; subst.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
-- 
cgit v1.2.3


From 4d3ecf1acd584200fe4299b8d12104c7acc33579 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 4 Dec 2018 11:31:39 -0500
Subject: Revert "Add subst to the end of nia in the test-suite"

This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01.

It turns out the 4x was due to .nia.cache (because I didn't clean
sufficiently in testing), not due to `subst`.
---
 doc/sphinx/addendum/micromega.rst | 3 +--
 test-suite/success/Nia.v          | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 5f199d28f5..2ace8a59e1 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -251,8 +251,7 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
 .. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by pre-processing the goal with
-  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.  Note that additionally
-  running ``subst`` can speed up things up, sometimees by almost 4x in practice.
+  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index c157173b77..6cb645d9eb 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -4,7 +4,7 @@ Open Scope Z_scope.
 
 (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; subst.
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
-- 
cgit v1.2.3


From 594e53cda3845794bf1e14aec7b0d2a5ee9cd075 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 5 Dec 2018 13:21:52 -0500
Subject: Update CHANGES

---
 CHANGES.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 6d76c857c9..cacf0e09e4 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -75,6 +75,11 @@ Tactics
   foo : database`). When the database name is omitted, the hint is added to the
   core database (as previously), but a deprecation warning is emitted.
 
+- There is now a tactic in `PreOmega.v` called `Z.div_mod_to_quot_rem`
+  which allows `lia`, `nia`, `romega`, etc to support `Z.div` and
+  `Z.modulo`, by posing the specifying equation for `Z.div` and
+  `Z.modulo` before replacing them with atoms.
+
 Vernacular commands
 
 - `Combined Scheme` can now work when inductive schemes are generated in sort
@@ -288,11 +293,6 @@ Standard Library
   impacts users running Coq without the init library (`-nois` or
   `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.
 
-- Tactic `zify` (and therefore `lia`, `nia`, `romega`, etc) now
-  supports `Z.div` and `Z.modulo` via the `Z.div_mod_to_quot_rem`
-  tactic in `PreOmega.v`, which poses the specifying equation for
-  `Z.div` and `Z.modulo` before replacing them with atoms.
-
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
-- 
cgit v1.2.3


From d69ec6e2e0931a87d2ec3b3f47d1969b365d91f7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 5 Dec 2018 16:05:13 -0500
Subject: Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations,
 Z.to_euclidean_division_equations

---
 CHANGES.md                        |  11 ++--
 doc/sphinx/addendum/micromega.rst |  12 +++-
 plugins/omega/PreOmega.v          | 118 +++++++++++++++++++++++++++++++++-----
 test-suite/success/Nia.v          |   8 ++-
 4 files changed, 127 insertions(+), 22 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index cacf0e09e4..54acb610bb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -75,10 +75,13 @@ Tactics
   foo : database`). When the database name is omitted, the hint is added to the
   core database (as previously), but a deprecation warning is emitted.
 
-- There is now a tactic in `PreOmega.v` called `Z.div_mod_to_quot_rem`
-  which allows `lia`, `nia`, `romega`, etc to support `Z.div` and
-  `Z.modulo`, by posing the specifying equation for `Z.div` and
-  `Z.modulo` before replacing them with atoms.
+- There are now tactics in `PreOmega.v` called
+  `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and
+  `Z.to_euclidean_division_equations` (which combines the `div_mod`
+  and `quot_rem` variants) which allow `lia`, `nia`, `romega`, etc to
+  support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively),
+  by posing the specifying equation for `Z.div` and `Z.modulo` before
+  replacing them with atoms.
 
 Vernacular commands
 
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 2ace8a59e1..b076aac1ed 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -250,8 +250,16 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
 .. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
-.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by pre-processing the goal with
-  the ``Z.div_mod_to_quot_rem`` tactic after manually running ``zify``.
+.. [#] Support for :g:`Z.div` and :g:`Z.modulo` may be obtained by
+  pre-processing the goal with the ``Z.div_mod_to_equations`` tactic (you may
+  need to manually run ``zify`` first).
+.. [#] Support for :g:`Z.quot` and :g:`Z.rem` may be obtained by pre-processing
+  the goal with the ``Z.quot_rem_to_equations`` tactic (you may need to manually
+  run ``zify`` first).
+.. [#] Note that support for :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and
+  :g:`Z.rem` may be simultaneously obtained by pre-processing the goal with the
+  ``Z.to_euclidean_division_equations`` tactic (you may need to manually run
+  ``zify`` first).
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 7ebc2fb04f..695f000cb1 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -12,12 +12,15 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat.
 
 Local Open Scope Z_scope.
 
-(** * [Z.div_mod_to_quot_rem]: the tactic for preprocessing [Z.div] and [Z.modulo] *)
+(** * [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] *)
 
-(** This tactic uses the complete specification of [Z.div] and
-    [Z.modulo] to remove these functions from the goal without losing
-    information.  The [Z.div_mod_to_quot_rem_cleanup] tactic removes
-    needless hypotheses, which makes tactics like [nia] run faster. *)
+(** 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.
@@ -25,7 +28,21 @@ Module Z.
   Lemma div_0_r_ext x y : y = 0 -> x / y = 0.
   Proof. intro; subst; destruct x; reflexivity. Qed.
 
-  Ltac div_mod_to_quot_rem_generalize x y :=
+  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);
@@ -36,23 +53,78 @@ Module Z.
     set (q := x / y) in *;
     set (r := x mod y) in *;
     clearbody q r.
-  Ltac div_mod_to_quot_rem_step :=
+  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_quot_rem_generalize x y
-    | [ |- context[?x mod ?y] ] => div_mod_to_quot_rem_generalize x y
-    | [ H : context[?x / ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
-    | [ H : context[?x mod ?y] |- _ ] => div_mod_to_quot_rem_generalize x y
+    | [ |- 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 div_mod_to_quot_rem' := repeat div_mod_to_quot_rem_step.
-  Ltac div_mod_to_quot_rem_cleanup :=
+  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_quot_rem := div_mod_to_quot_rem'; div_mod_to_quot_rem_cleanup.
+  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.
 
 (** * zify: the Z-ification tactic *)
@@ -453,6 +525,24 @@ Ltac zify_N_op :=
   | |- 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
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 6cb645d9eb..15028a4c00 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -2,9 +2,9 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 Open Scope Z_scope.
 
-(** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
+(** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
@@ -22,6 +22,10 @@ Ltac saturate_mod_div :=
          | [ H : context[?x mod ?y] |- _ ] => unique_pose_proof (Z_zerop_or (x / y))
          | [ |- context[?x / ?y] ] => unique_pose_proof (Z_zerop_or y)
          | [ H : context[?x / ?y] |- _ ] => unique_pose_proof (Z_zerop_or y)
+         | [ |- context[Z.rem ?x ?y] ] => unique_pose_proof (Z_zerop_or (Z.quot x y))
+         | [ H : context[Z.rem ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or (Z.quot x y))
+         | [ |- context[Z.quot ?x ?y] ] => unique_pose_proof (Z_zerop_or y)
+         | [ H : context[Z.quot ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or y)
          end.
 
 Ltac t := intros; saturate_mod_div; try nia.
-- 
cgit v1.2.3


From 687c7d97971316223e24b637973aa378077b5135 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 7 Dec 2018 01:41:03 -0500
Subject: Add some quot/rem test-cases for nia

---
 test-suite/success/Nia.v | 480 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 480 insertions(+)

diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 15028a4c00..62ecece792 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -436,3 +436,483 @@ Example Zdiv_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a /
 Example Z_div_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
 Example Z_div_small_iff: forall a b : Z, b <> 0 -> a / b = 0 <-> 0 <= a < b \/ b < a <= 0. Proof. intros; nia. Qed.
 Example Z_div_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed.
+
+(** Now we do the same, but with [Z.quot] and [Z.rem] instead. *)
+Lemma N2Z_inj_quot : forall n m : N, Z.of_N (n / m) = Z.of_N n ÷ Z.of_N m. Proof. intros; nia. Qed.
+Lemma N2Z_inj_rem : forall n m : N, Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m). Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0.
+Proof. intros; destruct (Z_zerop (a ÷ b)); nia. Qed.
+Lemma OrdersEx_Z_as_DT_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; destruct (Z_zerop (a ÷ b)); nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c).
+Proof. intros; assert (0 < b * c) by nia; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q.
+Proof.
+  intros.
+  destruct (Z_zerop p), (Z_zerop (p ÷ r)), (Z_zerop (p ÷ q)); subst; [ nia.. | ].
+  assert (0 < q) by nia; assert (0 < r) by nia; assert (0 < p) by nia.
+  nia.
+Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q.
+Proof.
+  intros.
+  destruct (Z_zerop p), (Z_zerop (p ÷ r)), (Z_zerop (p ÷ q)); [ subst; nia.. | ].
+  assert (0 < p) by nia; assert (0 < r) by nia.
+  nia.
+Qed.
+Lemma OrdersEx_Z_as_DT_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c.
+Proof.
+  intros.
+  destruct (Z_zerop a), (Z_zerop b), (Z_zerop (a ÷ c)), (Z_zerop (b ÷ c)); [ subst; nia.. | ].
+  nia.
+Qed.
+Lemma OrdersEx_Z_as_DT_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b.
+Proof.
+  intros.
+  assert (c * b <> 0) by nia.
+  destruct (Z_zerop a), (Z_zerop (c * a)); subst; [ nia | exfalso; nia.. | ].
+Abort.
+Lemma OrdersEx_Z_as_DT_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. Abort.
+Lemma OrdersEx_Z_as_DT_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; assert (b * c <> 0) by nia. Abort.
+Lemma OrdersEx_Z_as_DT_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_DT_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros. Fail nia. Abort.
+Lemma OrdersEx_Z_as_OT_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros. Fail nia. Abort.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros. Abort.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros. Fail nia. Abort.
+Lemma OrdersEx_Z_as_OT_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros. Fail nia. Abort.
+Lemma OrdersEx_Z_as_OT_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros. Abort.
+Lemma OrdersEx_Z_as_OT_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros. Abort.
+Lemma OrdersEx_Z_as_OT_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros. Abort.
+Lemma OrdersEx_Z_as_OT_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma OrdersEx_Z_as_OT_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z2N_inj_quot : forall n m : Z, 0 <= n -> 0 <= m -> Z.to_N (n ÷ m) = (Z.to_N n / Z.to_N m)%N.
+Proof. intros; destruct (Z_zerop n), (Z_zerop m), (Z_zerop (n ÷ m)); [ subst; try nia.. | ]. Abort.
+Lemma Z2N_inj_rem : forall n m : Z, 0 <= n -> 0 <= m -> Z.to_N (Z.rem n m) = (Z.to_N n mod Z.to_N m)%N. Proof. intros. Abort.
+Lemma Zabs2N_inj_quot : forall n m : Z, Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N. Proof. intros. Abort.
+Lemma Zabs2N_inj_rem : forall n m : Z, Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N. Proof. intros. Abort.
+(* Some of these don't work, and I haven't gone through and figured out which ones yet, so they're all commented out for now *)
+(*
+Lemma Z_add_rem : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma Z_add_rem_idemp_l : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma Z_add_rem_idemp_r : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (a + Z.rem b n) n = Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_add_rem : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (a + b) n = ZBinary.Z.rem (ZBinary.Z.rem a n + ZBinary.Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_add_rem_idemp_l : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (ZBinary.Z.rem a n + b) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_add_rem_idemp_r : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (a + ZBinary.Z.rem b n) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_gcd_quot_gcd : forall a b g : Z, g <> 0 -> g = ZBinary.Z.gcd a b -> ZBinary.Z.gcd (a ÷ g) (b ÷ g) = 1. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_gcd_rem : forall a b : Z, b <> 0 -> ZBinary.Z.gcd (ZBinary.Z.rem a b) b = ZBinary.Z.gcd b a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mod_mul_r : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem a (b * c) = ZBinary.Z.rem a b + b * ZBinary.Z.rem (a ÷ b) c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_pred_quot_gt : forall a b : Z, 0 <= a -> b < 0 -> a < b * ZBinary.Z.pred (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_pred_quot_lt : forall a b : Z, a <= 0 -> 0 < b -> b * ZBinary.Z.pred (a ÷ b) < a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_rem_distr_l : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem (c * a) (c * b) = c * ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_rem_distr_r : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem (a * c) (b * c) = ZBinary.Z.rem a b * c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_rem : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (a * b) n = ZBinary.Z.rem (ZBinary.Z.rem a n * ZBinary.Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_rem_idemp_l : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (ZBinary.Z.rem a n * b) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_rem_idemp_r : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (a * ZBinary.Z.rem b n) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_succ_quot_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * ZBinary.Z.succ (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_mul_succ_quot_lt : forall a b : Z, a <= 0 -> b < 0 -> b * ZBinary.Z.succ (a ÷ b) < a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_add_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a + b) n = ZBinary.Z.rem (ZBinary.Z.rem a n + ZBinary.Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_add_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n + b) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_add_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a + ZBinary.Z.rem b n) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_exact : forall a b : Z, 0 <= a -> 0 < b -> a = b * (a ÷ b) <-> ZBinary.Z.rem a b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_0_l : forall a : Z, 0 < a -> ZBinary.Z.rem 0 a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_1_l : forall a : Z, 1 < a -> ZBinary.Z.rem 1 a = 1. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_1_r : forall a : Z, 0 <= a -> ZBinary.Z.rem a 1 = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> ZBinary.Z.rem (a + b * c) c = ZBinary.Z.rem a c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_divides : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_le : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b <= a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_mod : forall a n : Z, 0 <= a -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n) n = ZBinary.Z.rem a n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_mul : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem (a * b) b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_mul_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem a (b * c) = ZBinary.Z.rem a b + b * ZBinary.Z.rem (a ÷ b) c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_same : forall a : Z, 0 < a -> ZBinary.Z.rem a a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_small : forall a b : Z, 0 <= a < b -> ZBinary.Z.rem a b = a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_small_iff : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = a <-> a < b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mod_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_distr_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem (c * a) (c * b) = c * ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_distr_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem (a * c) (b * c) = ZBinary.Z.rem a b * c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a * b) n = ZBinary.Z.rem (ZBinary.Z.rem a n * ZBinary.Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n * b) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a * ZBinary.Z.rem b n) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_NZQuot_mul_succ_div_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * ZBinary.Z.succ (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_Private_Div_Quot2Div_div_mod : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+ZBinary_Z_Private_Div_Quot2Div_div_wd  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) ZBinary.Z.quot
+Lemma ZBinary_Z_Private_Div_Quot2Div_mod_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= ZBinary.Z.rem a b < b. Proof. intros; nia. Qed.
+ZBinary_Z_Private_Div_Quot2Div_mod_wd  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) ZBinary.Z.rem
+Lemma ZBinary_Z_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_abs : forall a b : Z, b <> 0 -> ZBinary.Z.abs a ÷ ZBinary.Z.abs b = ZBinary.Z.abs (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_abs_l : forall a b : Z, b <> 0 -> ZBinary.Z.abs a ÷ b = ZBinary.Z.sgn a * (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_abs_r : forall a b : Z, b <> 0 -> a ÷ ZBinary.Z.abs b = ZBinary.Z.sgn b * (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_div : forall a b : Z, b <> 0 -> a ÷ b = ZBinary.Z.sgn a * ZBinary.Z.sgn b * (ZBinary.Z.abs a / ZBinary.Z.abs b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_exact : forall a b : Z, b <> 0 -> a = b * (a ÷ b) <-> ZBinary.Z.rem a b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_rem' : forall a b : Z, a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_rem : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_small_iff : forall a b : Z, b <> 0 -> a ÷ b = 0 <-> ZBinary.Z.abs a < ZBinary.Z.abs b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+ZBinary_Z_quot_wd  Morphisms.Proper (Morphisms.respectful ZBinary.Z.eq (Morphisms.respectful ZBinary.Z.eq ZBinary.Z.eq)) ZBinary.Z.quot
+Lemma ZBinary_Z_rem_0_l : forall a : Z, a <> 0 -> ZBinary.Z.rem 0 a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_1_l : forall a : Z, 1 < a -> ZBinary.Z.rem 1 a = 1. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_1_r : forall a : Z, ZBinary.Z.rem a 1 = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_abs : forall a b : Z, b <> 0 -> ZBinary.Z.rem (ZBinary.Z.abs a) (ZBinary.Z.abs b) = ZBinary.Z.abs (ZBinary.Z.rem a b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_abs_l : forall a b : Z, b <> 0 -> ZBinary.Z.rem (ZBinary.Z.abs a) b = ZBinary.Z.abs (ZBinary.Z.rem a b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_abs_r : forall a b : Z, b <> 0 -> ZBinary.Z.rem a (ZBinary.Z.abs b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> ZBinary.Z.rem (a + b * c) c = ZBinary.Z.rem a c. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_bound_abs : forall a b : Z, b <> 0 -> ZBinary.Z.abs (ZBinary.Z.rem a b) < ZBinary.Z.abs b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= ZBinary.Z.rem a b < b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_eq : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = a - b * (a ÷ b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_le : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b <= a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_mod_eq_0 : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_mod : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = ZBinary.Z.sgn a * (ZBinary.Z.abs a mod ZBinary.Z.abs b). Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_mod_nonneg : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = a mod b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_mul : forall a b : Z, b <> 0 -> ZBinary.Z.rem (a * b) b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_nonneg : forall a b : Z, b <> 0 -> 0 <= a -> 0 <= ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_nonpos : forall a b : Z, b <> 0 -> a <= 0 -> ZBinary.Z.rem a b <= 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_opp_l : forall a b : Z, b <> 0 -> ZBinary.Z.rem (- a) b = - ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_opp_l' : forall a b : Z, ZBinary.Z.rem (- a) b = - ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_opp_opp : forall a b : Z, b <> 0 -> ZBinary.Z.rem (- a) (- b) = - ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_opp_r : forall a b : Z, b <> 0 -> ZBinary.Z.rem a (- b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_opp_r' : forall a b : Z, ZBinary.Z.rem a (- b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_quot : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b ÷ b = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_rem : forall a n : Z, n <> 0 -> ZBinary.Z.rem (ZBinary.Z.rem a n) n = ZBinary.Z.rem a n. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_same : forall a : Z, a <> 0 -> ZBinary.Z.rem a a = 0. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_sign : forall a b : Z, a <> 0 -> b <> 0 -> ZBinary.Z.sgn (ZBinary.Z.rem a b) <> - ZBinary.Z.sgn a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_sign_mul : forall a b : Z, b <> 0 -> 0 <= ZBinary.Z.rem a b * a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_sign_nz : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b <> 0 -> ZBinary.Z.sgn (ZBinary.Z.rem a b) = ZBinary.Z.sgn a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_small : forall a b : Z, 0 <= a < b -> ZBinary.Z.rem a b = a. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_small_iff : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = a <-> ZBinary.Z.abs a < ZBinary.Z.abs b. Proof. intros; nia. Qed.
+Lemma ZBinary_Z_rem_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = ZBinary.Z.rem a b. Proof. intros; nia. Qed.
+ZBinary_Z_rem_wd  Morphisms.Proper (Morphisms.respectful ZBinary.Z.eq (Morphisms.respectful ZBinary.Z.eq ZBinary.Z.eq)) ZBinary.Z.rem
+Lemma Z_gcd_quot_gcd : forall a b g : Z, g <> 0 -> g = Z.gcd a b -> Z.gcd (a ÷ g) (b ÷ g) = 1. Proof. intros; nia. Qed.
+Lemma Z_gcd_rem : forall a b : Z, b <> 0 -> Z.gcd (Z.rem a b) b = Z.gcd b a. Proof. intros; nia. Qed.
+Lemma Z_mod_mul_r : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem a (b * c) = Z.rem a b + b * Z.rem (a ÷ b) c. Proof. intros; nia. Qed.
+Lemma Z_mul_pred_quot_gt : forall a b : Z, 0 <= a -> b < 0 -> a < b * Z.pred (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_mul_pred_quot_lt : forall a b : Z, a <= 0 -> 0 < b -> b * Z.pred (a ÷ b) < a. Proof. intros; nia. Qed.
+Lemma Z_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed.
+Lemma Z_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed.
+Lemma Z_mul_rem_distr_l : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_mul_rem_distr_r : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed.
+Lemma Z_mul_rem : forall a b n : Z, n <> 0 -> Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma Z_mul_rem_idemp_l : forall a b n : Z, n <> 0 -> Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma Z_mul_rem_idemp_r : forall a b n : Z, n <> 0 -> Z.rem (a * Z.rem b n) n = Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma Z_mul_succ_quot_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * Z.succ (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_mul_succ_quot_lt : forall a b : Z, a <= 0 -> b < 0 -> b * Z.succ (a ÷ b) < a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_add_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_add_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_add_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a + Z.rem b n) n = Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_exact : forall a b : Z, 0 <= a -> 0 < b -> a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_0_l : forall a : Z, 0 < a -> Z.rem 0 a = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_1_l : forall a : Z, 1 < a -> Z.rem 1 a = 1. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_1_r : forall a : Z, 0 <= a -> Z.rem a 1 = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_divides : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_le : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b <= a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_mod : forall a n : Z, 0 <= a -> 0 < n -> Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_mul : forall a b : Z, 0 <= a -> 0 < b -> Z.rem (a * b) b = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_mul_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem a (b * c) = Z.rem a b + b * Z.rem (a ÷ b) c. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_same : forall a : Z, 0 < a -> Z.rem a a = 0. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_small : forall a b : Z, 0 <= a < b -> Z.rem a b = a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_small_iff : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a <-> a < b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mod_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mul_mod_distr_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mul_mod_distr_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mul_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mul_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mul_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a * Z.rem b n) n = Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma Z_Private_Div_NZQuot_mul_succ_div_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * Z.succ (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_Private_Div_Quot2Div_div_mod : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed.
+Z_Private_Div_Quot2Div_div_wd  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) Z.quot
+Lemma Z_Private_Div_Quot2Div_mod_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed.
+Z_Private_Div_Quot2Div_mod_wd  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) Z.rem
+Lemma Z_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma Z_quot_0_r_ext : forall x y : Z, y = 0 -> x ÷ y = 0. Proof. intros; nia. Qed.
+Lemma Z_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma Z_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed.
+Lemma Zquot2_quot : forall n : Z, Z.quot2 n = n ÷ 2. Proof. intros; nia. Qed.
+Lemma Z_quot_abs : forall a b : Z, b <> 0 -> Z.abs a ÷ Z.abs b = Z.abs (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_quot_abs_l : forall a b : Z, b <> 0 -> Z.abs a ÷ b = Z.sgn a * (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_quot_abs_r : forall a b : Z, b <> 0 -> a ÷ Z.abs b = Z.sgn b * (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma Z_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_div : forall a b : Z, b <> 0 -> a ÷ b = Z.sgn a * Z.sgn b * (Z.abs a / Z.abs b). Proof. intros; nia. Qed.
+Lemma Z_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed.
+Lemma Z_quot_exact : forall a b : Z, b <> 0 -> a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed.
+Lemma Z_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed.
+Lemma Z_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed.
+Lemma Z_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma Z_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma Z_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma Z_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed.
+Lemma Z_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed.
+Lemma Z_quot_rem' : forall a b : Z, a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_quot_rem : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed.
+Lemma Z_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed.
+Lemma Z_quot_small_iff : forall a b : Z, b <> 0 -> a ÷ b = 0 <-> Z.abs a < Z.abs b. Proof. intros; nia. Qed.
+Lemma Z_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma Z_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Z_quot_wd  Morphisms.Proper (Morphisms.respectful Z.eq (Morphisms.respectful Z.eq Z.eq)) Z.quot
+Lemma Zquot_Zeven_rem : forall a : Z, Z.even a = (Z.rem a 2 =? 0). Proof. intros; nia. Qed.
+Lemma Zquot_Z_mult_quot_ge : forall a b : Z, a <= 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed.
+Lemma Zquot_Z_mult_quot_le : forall a b : Z, 0 <= a -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed.
+Lemma Zquot_Zmult_rem_distr_l : forall a b c : Z, Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed.
+Lemma Zquot_Zmult_rem_distr_r : forall a b c : Z, Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed.
+Lemma Zquot_Zmult_rem : forall a b n : Z, Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma Zquot_Zmult_rem_idemp_l : forall a b n : Z, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed.
+Lemma Zquot_Zmult_rem_idemp_r : forall a b n : Z, Z.rem (b * Z.rem a n) n = Z.rem (b * a) n. Proof. intros; nia. Qed.
+Lemma Zquot_Zodd_rem : forall a : Z, Z.odd a = negb (Z.rem a 2 =? 0). Proof. intros; nia. Qed.
+Lemma Zquot_Zplus_rem : forall a b n : Z, 0 <= a * b -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed.
+Lemma Zquot_Zplus_rem_idemp_l : forall a b n : Z, 0 <= a * b -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed.
+Lemma Zquot_Zplus_rem_idemp_r : forall a b n : Z, 0 <= a * b -> Z.rem (b + Z.rem a n) n = Z.rem (b + a) n. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_0_l : forall a : Z, 0 ÷ a = 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_0_r : forall a : Z, a ÷ 0 = 0. Proof. intros; nia. Qed.
+Lemma Zquot_Z_quot_exact_full : forall a b : Z, a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_le_lower_bound : forall a b q : Z, 0 < b -> q * b <= a -> q <= a ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_le_upper_bound : forall a b q : Z, 0 < b -> a <= q * b -> a ÷ b <= q. Proof. intros; nia. Qed.
+Lemma Zquot_Z_quot_lt : forall a b : Z, 0 < a -> 2 <= b -> a ÷ b < a. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < q * b -> a ÷ b < q. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_mod_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> q = a ÷ b /\ r = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Zquot_Z_quot_monotone : forall a b c : Z, 0 <= c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_mult_cancel_l : forall a b c : Z, c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_mult_cancel_r : forall a b c : Z, c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_mult_le : forall a b c : Z, 0 <= a -> 0 <= b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_opp_l : forall a b : Z, - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_opp_opp : forall a b : Z, - a ÷ - b = a ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_opp_r : forall a b : Z, a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed.
+Lemma Zquot_Z_quot_plus : forall a b c : Z, 0 <= (a + b * c) * a -> c <> 0 -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed.
+Lemma Zquot_Z_quot_plus_l : forall a b c : Z, 0 <= (a * b + c) * c -> b <> 0 -> b <> 0 -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Z_quot_pos : forall a b : Z, 0 <= a -> 0 <= b -> 0 <= a ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquotrem_Zdiv_eucl_pos : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b /\ Z.rem a b = a mod b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_sgn : forall a b : Z, 0 <= Z.sgn (a ÷ b) * Z.sgn a * Z.sgn b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_Zdiv_pos : forall a b : Z, 0 <= a -> 0 <= b -> a ÷ b = a / b. Proof. intros; nia. Qed.
+Lemma Zquot_Zquot_Zquot : forall a b c : Z, a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_0_l : forall a : Z, Z.rem 0 a = 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_0_r : forall a : Z, Z.rem a 0 = a. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_divides : forall a b : Z, Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_even : forall a : Z, Z.rem a 2 = (if Z.even a then 0 else Z.sgn a). Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_le : forall a b : Z, 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_lt_neg : forall a b : Z, a <= 0 -> b <> 0 -> - Z.abs b < Z.rem a b <= 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_lt_neg_neg : forall a b : Z, a <= 0 -> b < 0 -> b < Z.rem a b <= 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_lt_neg_pos : forall a b : Z, a <= 0 -> 0 < b -> - b < Z.rem a b <= 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_lt_pos : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_lt_pos_neg : forall a b : Z, 0 <= a -> b < 0 -> 0 <= Z.rem a b < - b. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_lt_pos_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed.
+Lemma Zquot_Z_rem_mult : forall a b : Z, Z.rem (a * b) b = 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_odd : forall a : Z, Z.rem a 2 = (if Z.odd a then Z.sgn a else 0). Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_opp_l : forall a b : Z, Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_opp_opp : forall a b : Z, Z.rem (- a) (- b) = - Z.rem a b. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_opp_r : forall a b : Z, Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Zquot_Z_rem_plus : forall a b c : Z, 0 <= (a + b * c) * a -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_rem : forall a n : Z, Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed.
+Lemma Zquot_Z_rem_same : forall a : Z, Z.rem a a = 0. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_sgn2 : forall a b : Z, 0 <= Z.rem a b * a. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_sgn : forall a b : Z, 0 <= Z.sgn (Z.rem a b) * Z.sgn a. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_Zmod_pos : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b. Proof. intros; nia. Qed.
+Lemma Zquot_Zrem_Zmod_zero : forall a b : Z, b <> 0 -> Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed.
+Lemma Z_rem_0_l : forall a : Z, a <> 0 -> Z.rem 0 a = 0. Proof. intros; nia. Qed.
+Lemma Z_rem_0_r_ext : forall x y : Z, y = 0 -> Z.rem x y = x. Proof. intros; nia. Qed.
+Lemma Z_rem_1_l : forall a : Z, 1 < a -> Z.rem 1 a = 1. Proof. intros; nia. Qed.
+Lemma Z_rem_1_r : forall a : Z, Z.rem a 1 = 0. Proof. intros; nia. Qed.
+Lemma Z_rem_abs : forall a b : Z, b <> 0 -> Z.rem (Z.abs a) (Z.abs b) = Z.abs (Z.rem a b). Proof. intros; nia. Qed.
+Lemma Z_rem_abs_l : forall a b : Z, b <> 0 -> Z.rem (Z.abs a) b = Z.abs (Z.rem a b). Proof. intros; nia. Qed.
+Lemma Z_rem_abs_r : forall a b : Z, b <> 0 -> Z.rem a (Z.abs b) = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed.
+Lemma Z_rem_bound_abs : forall a b : Z, b <> 0 -> Z.abs (Z.rem a b) < Z.abs b. Proof. intros; nia. Qed.
+Lemma Z_rem_bound_neg_neg : forall x y : Z, y < 0 -> x <= 0 -> y < Z.rem x y <= 0. Proof. intros; nia. Qed.
+Lemma Z_rem_bound_neg_pos : forall x y : Z, y < 0 -> 0 <= x -> 0 <= Z.rem x y < - y. Proof. intros; nia. Qed.
+Lemma Z_rem_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed.
+Lemma Z_rem_bound_pos_neg : forall x y : Z, 0 < y -> x <= 0 -> - y < Z.rem x y <= 0. Proof. intros; nia. Qed.
+Lemma Z_rem_bound_pos_pos : forall x y : Z, 0 < y -> 0 <= x -> 0 <= Z.rem x y < y. Proof. intros; nia. Qed.
+Lemma Z_rem_eq : forall a b : Z, b <> 0 -> Z.rem a b = a - b * (a ÷ b). Proof. intros; nia. Qed.
+Lemma Z_rem_le : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b <= a. Proof. intros; nia. Qed.
+Lemma Z_rem_mod_eq_0 : forall a b : Z, b <> 0 -> Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed.
+Lemma Z_rem_mod : forall a b : Z, b <> 0 -> Z.rem a b = Z.sgn a * (Z.abs a mod Z.abs b). Proof. intros; nia. Qed.
+Lemma Z_rem_mod_nonneg : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b. Proof. intros; nia. Qed.
+Lemma Z_rem_mul : forall a b : Z, b <> 0 -> Z.rem (a * b) b = 0. Proof. intros; nia. Qed.
+Lemma Z_rem_nonneg : forall a b : Z, b <> 0 -> 0 <= a -> 0 <= Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_nonpos : forall a b : Z, b <> 0 -> a <= 0 -> Z.rem a b <= 0. Proof. intros; nia. Qed.
+Lemma Z_rem_opp_l : forall a b : Z, b <> 0 -> Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_opp_l' : forall a b : Z, Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_opp_opp : forall a b : Z, b <> 0 -> Z.rem (- a) (- b) = - Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_opp_r : forall a b : Z, b <> 0 -> Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_opp_r' : forall a b : Z, Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_quot : forall a b : Z, b <> 0 -> Z.rem a b ÷ b = 0. Proof. intros; nia. Qed.
+Lemma Z_rem_rem : forall a n : Z, n <> 0 -> Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed.
+Lemma Z_rem_same : forall a : Z, a <> 0 -> Z.rem a a = 0. Proof. intros; nia. Qed.
+Lemma Z_rem_sign : forall a b : Z, a <> 0 -> b <> 0 -> Z.sgn (Z.rem a b) <> - Z.sgn a. Proof. intros; nia. Qed.
+Lemma Z_rem_sign_mul : forall a b : Z, b <> 0 -> 0 <= Z.rem a b * a. Proof. intros; nia. Qed.
+Lemma Z_rem_sign_nz : forall a b : Z, b <> 0 -> Z.rem a b <> 0 -> Z.sgn (Z.rem a b) = Z.sgn a. Proof. intros; nia. Qed.
+Lemma Z_rem_small : forall a b : Z, 0 <= a < b -> Z.rem a b = a. Proof. intros; nia. Qed.
+Lemma Z_rem_small_iff : forall a b : Z, b <> 0 -> Z.rem a b = a <-> Z.abs a < Z.abs b. Proof. intros; nia. Qed.
+Lemma Z_rem_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed.
+Lemma Z_rem_wd : Morphisms.Proper (Morphisms.respectful Z.eq (Morphisms.respectful Z.eq Z.eq)) Z.rem. Proof. intros; nia. Qed.
+*)
-- 
cgit v1.2.3