Add versions of ZUtil lemmas without nonzero assumptions

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
2m38.91s | Total                                           | 2m40.89s || -0m01.97s
----------------------------------------------------------------------------------
0m17.80s | ModularArithmetic/ModularBaseSystemProofs       | 0m25.90s || -0m08.09s
0m25.51s | ModularArithmetic/Pow2BaseProofs                | 0m23.25s || +0m02.26s
0m15.42s | Experiments/SpecEd25519                         | 0m13.98s || +0m01.43s
0m11.16s | Util/ZUtil                                      | 0m12.18s || -0m01.01s
0m10.54s | ModularArithmetic/Montgomery/ZProofs            | 0m08.81s || +0m01.72s
0m10.22s | Specific/GF25519                                | 0m10.69s || -0m00.46s
0m09.68s | Testbit                                         | 0m09.06s || +0m00.61s
0m06.84s | Specific/GF1305                                 | 0m06.97s || -0m00.12s
0m05.08s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m04.74s || +0m00.33s
0m04.91s | BaseSystemProofs                                | 0m04.90s || +0m00.00s
0m04.57s | ModularArithmetic/Tutorial                      | 0m05.05s || -0m00.47s
0m04.07s | ModularArithmetic/ModularArithmeticTheorems     | 0m03.09s || +0m00.98s
0m03.68s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m04.53s || -0m00.85s
0m03.31s | Experiments/SpecificCurve25519                  | 0m03.29s || +0m00.02s
0m02.81s | ModularArithmetic/BarrettReduction/ZBounded     | 0m02.28s || +0m00.53s
0m02.33s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.32s || +0m00.01s
0m01.82s | ModularArithmetic/BarrettReduction/Z            | 0m02.10s || -0m00.28s
0m01.76s | BaseSystem                                      | 0m01.28s || +0m00.48s
0m01.66s | Encoding/PointEncodingPre                       | 0m01.70s || -0m00.04s
0m01.60s | ModularArithmetic/PrimeFieldTheorems            | 0m01.10s || +0m00.50s
0m01.34s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.02s || +0m00.32s
0m01.30s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.89s || +0m00.41s
0m01.21s | ModularArithmetic/ExtendedBaseVector            | 0m01.16s || +0m00.05s
0m00.99s | Util/NumTheoryUtil                              | 0m00.97s || +0m00.02s
0m00.92s | ModularArithmetic/Montgomery/ZBounded           | 0m00.85s || +0m00.07s
0m00.86s | ModularArithmetic/ModularBaseSystemField        | 0m00.91s || -0m00.05s
0m00.76s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.65s || +0m00.10s
0m00.75s | Encoding/ModularWordEncodingPre                 | 0m00.69s || +0m00.06s
0m00.71s | ModularArithmetic/ZBounded                      | 0m00.66s || +0m00.04s
0m00.68s | Encoding/ModularWordEncodingTheorems            | 0m00.69s || -0m00.00s
0m00.64s | ModularArithmetic/ModularBaseSystem             | 0m00.89s || -0m00.25s
0m00.63s | Spec/ModularWordEncoding                        | 0m00.63s || +0m00.00s
0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.59s || +0m00.01s
0m00.59s | ModularArithmetic/ModularBaseSystemList         | 0m00.65s || -0m00.06s
0m00.49s | ModularArithmetic/Pre                           | 0m00.49s || +0m00.00s
0m00.45s | ModularArithmetic/Pow2Base                      | 0m00.46s || -0m00.01s
0m00.44s | ModularArithmetic/Montgomery/Z                  | 0m00.46s || -0m00.02s
0m00.40s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.44s || -0m00.03s
0m00.39s | Spec/ModularArithmetic                          | 0m00.57s || -0m00.17s

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 415d70d65..9a6080cda 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1618,6 +1618,18 @@ Module Z.
   Proof. intros; rewrite (mod_small_n 1) by lia; lia. Qed.
   Hint Rewrite mod_small_1 using zutil_arith : zsimplify.
 
+  Lemma mul_mod_distr_r_full a b c : (a * c) mod (b * c) = (a mod b * c).
+  Proof.
+    destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst;
+      autorewrite with zsimplify; auto using Z.mul_mod_distr_r.
+  Qed.
+
+  Lemma mul_mod_distr_l_full a b c : (c * a) mod (c * b) = c * (a mod b).
+  Proof.
+    destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst;
+      autorewrite with zsimplify; auto using Z.mul_mod_distr_l.
+  Qed.
+
   Lemma leb_add_same x y : (x <=? y + x) = (0 <=? y).
   Proof. destruct (x <=? y + x) eqn:?, (0 <=? y) eqn:?; ltb_to_lt; try reflexivity; omega. Qed.
   Hint Rewrite leb_add_same : zsimplify.