Shuffle some ZUtil lemmas around

_CoqProject

@@ -6597,6 +6597,7 @@ src/Util/ZUtil/EquivModulo.v
 src/Util/ZUtil/Ge.v
 src/Util/ZUtil/Hints.v
 src/Util/ZUtil/Land.v
+src/Util/ZUtil/Le.v
 src/Util/ZUtil/ModInv.v
 src/Util/ZUtil/Modulo.v
 src/Util/ZUtil/Morphisms.v

src/Experiments/NewPipeline/Arithmetic.v

@@ -2247,7 +2247,7 @@ Module BaseConversion.
       eval dw dn (convert_bases sn dn p) = eval sw sn p.
     Proof using dwprops.
       cbv [convert_bases]; intros.
-      rewrite eval_chained_carries_no_reduce; auto using ZUtil.Z.positive_is_nonzero.
+      rewrite eval_chained_carries_no_reduce; auto using Z.positive_is_nonzero.
       rewrite eval_from_associational; auto.
     Qed.
 

src/Experiments/SimplyTypedArithmetic.v

@@ -1759,7 +1759,7 @@ Module BaseConversion.
       eval dw dn (convert_bases sn dn p) = eval sw sn p.
     Proof.
       cbv [convert_bases]; intros.
-      rewrite eval_chained_carries_no_reduce; auto using ZUtil.Z.positive_is_nonzero.
+      rewrite eval_chained_carries_no_reduce; auto using Z.positive_is_nonzero.
       rewrite eval_from_associational; auto.
     Qed.
 

src/Util/ZUtil.v

@@ -13,6 +13,7 @@ Require Import Coq.Lists.List.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Export Crypto.Util.ZUtil.Definitions.
 Require Export Crypto.Util.ZUtil.Div.
+Require Export Crypto.Util.ZUtil.Le.
 Require Export Crypto.Util.ZUtil.EquivModulo.
 Require Export Crypto.Util.ZUtil.Hints.
 Require Export Crypto.Util.ZUtil.Land.
@@ -30,26 +31,9 @@ Import Nat.
 Local Open Scope Z.
 
 Module Z.
-  Lemma div_lt_upper_bound' a b q : 0 < b -> a < q * b -> a / b < q.
-  Proof. intros; apply Z.div_lt_upper_bound; nia. Qed.
-  Hint Resolve div_lt_upper_bound' : zarith.
-
   Lemma mul_comm3 x y z : x * (y * z) = y * (x * z).
   Proof. lia. Qed.
 
-  Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
-  Proof. intros; omega. Qed.
-  Hint Resolve positive_is_nonzero : zarith.
-
-  Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
-    a / b > 0.
-  Proof.
-    intros; rewrite Z.gt_lt_iff.
-    apply Z.div_str_pos.
-    split; intuition auto with omega.
-    apply Z.divide_pos_le; try (apply Zmod_divide); omega.
-  Qed.
-
   Lemma pos_pow_nat_pos : forall x n,
     Z.pos x ^ Z.of_nat n > 0.
   Proof.
@@ -59,7 +43,7 @@ Module Z.
   Qed.
 
   (** TODO: Should we get rid of this duplicate? *)
-  Notation gt0_neq0 := positive_is_nonzero (only parsing).
+  Notation gt0_neq0 := Z.positive_is_nonzero (only parsing).
 
   Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
     ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
@@ -708,19 +692,6 @@ Module Z.
   Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X.
   Proof. lia. Qed.
 
-  Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1).
-  Proof.
-    destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity.
-  Qed.
-
-  Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1).
-  Proof.
-    destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia.
-  Qed.
-
-  Hint Rewrite Z.div_opp_l_complete using zutil_arith : pull_Zopp.
-  Hint Rewrite Z.div_opp_l_complete' using zutil_arith : push_Zopp.
-
   Lemma shiftl_opp_l a n
     : Z.shiftl (-a) n = - Z.shiftl a n - (if Z_zerop (a mod 2 ^ (- n)) then 0 else 1).
   Proof.
@@ -747,18 +718,6 @@ Module Z.
   Hint Rewrite shiftr_opp_l : push_Zshift.
   Hint Rewrite <- shiftr_opp_l : pull_Zshift.
 
-  Lemma div_opp a : a <> 0 -> -a / a = -1.
-  Proof.
-    intros; autorewrite with pull_Zopp zsimplify; lia.
-  Qed.
-
-  Hint Rewrite Z.div_opp using zutil_arith : zsimplify.
-
-  Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0.
-  Proof. auto with zarith lia. Qed.
-
-  Hint Rewrite div_sub_1_0 using zutil_arith : zsimplify.
-
   Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0.
   Proof.
     intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1).
@@ -805,12 +764,6 @@ Module Z.
   Qed.
   Hint Resolve mod_eq_le_to_eq : zarith.
 
-  Lemma div_same' a b : b <> 0 -> a = b -> a / b = 1.
-  Proof.
-    intros; subst; auto with zarith.
-  Qed.
-  Hint Resolve div_same' : zarith.
-
   Lemma mod_eq_le_div_1 a b : 0 < a <= b -> a mod b = 0 -> a / b = 1.
   Proof. auto with zarith. Qed.
   Hint Resolve mod_eq_le_div_1 : zarith.

src/Util/ZUtil/Div.v

@@ -1,5 +1,8 @@
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Coq.ZArith.Znumtheory.
 Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn.
+Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
+Require Import Crypto.Util.ZUtil.Le.
 Require Import Crypto.Util.ZUtil.Hints.Core.
 Require Import Crypto.Util.ZUtil.Hints.ZArith.
 Require Import Crypto.Util.ZUtil.Hints.PullPush.
@@ -187,4 +190,72 @@ Module Z.
     intros; rewrite !Z.div_div by omega.
     f_equal; ring.
   Qed.
+
+  Lemma div_lt_upper_bound' a b q : 0 < b -> a < q * b -> a / b < q.
+  Proof. intros; apply Z.div_lt_upper_bound; nia. Qed.
+  Hint Resolve div_lt_upper_bound' : zarith.
+
+  Lemma div_cross_le_abs a b c' d : c' <> 0 -> d <> 0 -> a * Z.sgn c' * Z.abs d <= b * Z.sgn d * Z.abs c' -> a / c' <= b / d.
+  Proof.
+    clear.
+    destruct c', d; cbn [Z.abs Z.sgn];
+      rewrite ?Zdiv_0_r, ?Z.mul_0_r, ?Z.mul_0_l, ?Z.mul_1_l, ?Z.mul_1_r;
+      try lia; intros ?? H;
+        Z.div_mod_to_quot_rem;
+        subst.
+    all: repeat match goal with
+                | [ H : context[_ * -1] |- _ ] => rewrite (Z.mul_add_distr_r _ _ (-1)), <- ?(Z.mul_comm (-1)), ?Z.mul_assoc in H
+                | [ H : context[-1 * _] |- _ ] => rewrite (Z.mul_add_distr_l (-1)), <- ?(Z.mul_comm (-1)), ?Z.mul_assoc in H
+                | [ H : context[-1 * Z.neg ?x] |- _ ] => rewrite (Z.mul_comm (-1) (Z.neg x)), <- Z.opp_eq_mul_m1 in H
+                | [ H : context[-1 * ?x] |- _ ] => rewrite (Z.mul_comm (-1) x), <- Z.opp_eq_mul_m1 in H
+                | [ H : context[-Z.neg _] |- _ ] => cbn [Z.opp] in H
+                end.
+    all:lazymatch goal with
+        | [ H : (Z.pos ?p * ?q + ?r) * Z.pos ?p' <= (Z.pos ?p' * ?q' + ?r') * Z.pos ?p |- _ ]
+          => let H' := fresh in
+             assert (H' : q <= q' + (r' * Z.pos p - r * Z.pos p') / (Z.pos p * Z.pos p')) by (Z.div_mod_to_quot_rem; nia);
+               revert H'
+        end.
+    all:Z.div_mod_to_quot_rem; nia.
+  Qed.
+
+  Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
+    a / b > 0.
+  Proof.
+    intros; rewrite Z.gt_lt_iff.
+    apply Z.div_str_pos.
+    split; intuition auto with omega.
+    apply Z.divide_pos_le; try (apply Zmod_divide); omega.
+  Qed.
+
+  Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1).
+  Proof.
+    destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity.
+  Qed.
+
+  Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1).
+  Proof.
+    destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia.
+  Qed.
+
+  Hint Rewrite Z.div_opp_l_complete using zutil_arith : pull_Zopp.
+  Hint Rewrite Z.div_opp_l_complete' using zutil_arith : push_Zopp.
+
+  Lemma div_opp a : a <> 0 -> -a / a = -1.
+  Proof.
+    intros; autorewrite with pull_Zopp zsimplify; lia.
+  Qed.
+
+  Hint Rewrite Z.div_opp using zutil_arith : zsimplify.
+
+  Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0.
+  Proof. auto with zarith lia. Qed.
+
+  Hint Rewrite div_sub_1_0 using zutil_arith : zsimplify.
+
+  Lemma div_same' a b : b <> 0 -> a = b -> a / b = 1.
+  Proof.
+    intros; subst; auto with zarith.
+  Qed.
+  Hint Resolve div_same' : zarith.
 End Z.

src/Util/ZUtil/Le.v

@@ -0,0 +1,9 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
+  Proof. intros; omega. Qed.
+  Hint Resolve positive_is_nonzero : zarith.
+End Z.