Add {push,pull}_Zdiv databases

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m43.16s | Total                                           | 1m44.38s || -0m01.21s
----------------------------------------------------------------------------------
0m15.14s | ModularArithmetic/ModularBaseSystemProofs       | 0m16.70s || -0m01.55s
0m32.63s | Specific/GF25519                                | 0m32.58s || +0m00.05s
0m11.49s | Experiments/SpecEd25519                         | 0m11.35s || +0m00.14s
0m07.46s | Specific/GF1305                                 | 0m07.13s || +0m00.33s
0m04.06s | ModularArithmetic/Pow2BaseProofs                | 0m04.02s || +0m00.04s
0m03.72s | ModularArithmetic/Tutorial                      | 0m03.70s || +0m00.02s
0m03.71s | BaseSystemProofs                                | 0m03.68s || +0m00.02s
0m03.21s | ModularArithmetic/ModularBaseSystemOpt          | 0m03.24s || -0m00.03s
0m02.70s | Util/ZUtil                                      | 0m02.75s || -0m00.04s
0m01.59s | ModularArithmetic/PrimeFieldTheorems            | 0m01.53s || +0m00.06s
0m01.57s | ModularArithmetic/ModularArithmeticTheorems     | 0m01.54s || +0m00.03s
0m01.51s | Encoding/PointEncodingPre                       | 0m01.48s || +0m00.03s
0m01.18s | BaseSystem                                      | 0m01.18s || +0m00.00s
0m01.14s | ModularArithmetic/ExtendedBaseVector            | 0m01.09s || +0m00.04s
0m00.98s | Experiments/DerivationsOptionRectLetInEncoding  | 0m00.96s || +0m00.02s
0m00.96s | ModularArithmetic/BarrettReduction/Z            | 0m00.95s || +0m00.01s
0m00.86s | ModularArithmetic/ModularBaseSystemField        | 0m00.92s || -0m00.06s
0m00.85s | Util/NumTheoryUtil                              | 0m00.86s || -0m00.01s
0m00.84s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.83s || +0m00.01s
0m00.83s | ModularArithmetic/ModularBaseSystemList         | 0m00.88s || -0m00.05s
0m00.71s | Experiments/SpecificCurve25519                  | 0m00.70s || +0m00.01s
0m00.68s | Encoding/ModularWordEncodingTheorems            | 0m00.66s || +0m00.02s
0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.94s || -0m00.28s
0m00.65s | Testbit                                         | 0m00.65s || +0m00.00s
0m00.63s | Spec/ModularWordEncoding                        | 0m00.60s || +0m00.03s
0m00.63s | Encoding/ModularWordEncodingPre                 | 0m00.65s || -0m00.02s
0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.60s || +0m00.00s
0m00.57s | ModularArithmetic/ModularBaseSystem             | 0m00.57s || +0m00.00s
0m00.47s | ModularArithmetic/Pre                           | 0m00.46s || +0m00.00s
0m00.39s | ModularArithmetic/Pow2Base                      | 0m00.42s || -0m00.02s
0m00.38s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.40s || -0m00.02s
0m00.38s | Spec/ModularArithmetic                          | 0m00.36s || +0m00.02s

1 files changed, 6 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 1e0ed36e4..773a4818d 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -35,6 +35,8 @@ Create HintDb push_Zpow discriminated.
 Create HintDb pull_Zpow discriminated.
 Create HintDb push_Zmul discriminated.
 Create HintDb pull_Zmul discriminated.
+Create HintDb push_Zdiv discriminated.
+Create HintDb pull_Zdiv discriminated.
 Create HintDb pull_Zmod discriminated.
 Create HintDb push_Zmod discriminated.
 Hint Extern 1 => autorewrite with push_Zopp in * : push_Zopp.
@@ -43,6 +45,8 @@ Hint Extern 1 => autorewrite with push_Zpow in * : push_Zpow.
 Hint Extern 1 => autorewrite with pull_Zpow in * : pull_Zpow.
 Hint Extern 1 => autorewrite with push_Zmul in * : push_Zmul.
 Hint Extern 1 => autorewrite with pull_Zmul in * : pull_Zmul.
+Hint Extern 1 => autorewrite with push_Zdiv in * : push_Zmul.
+Hint Extern 1 => autorewrite with pull_Zdiv in * : pull_Zmul.
 Hint Extern 1 => autorewrite with pull_Zmod in * : pull_Zmod.
 Hint Extern 1 => autorewrite with push_Zmod in * : push_Zmod.
 Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp.
@@ -55,6 +59,8 @@ Hint Rewrite Z.pow_sub_r Z.pow_div_l Z.pow_twice_r Z.pow_mul_l Z.pow_add_r using
 Hint Rewrite <- Z.pow_sub_r Z.pow_div_l Z.pow_mul_l Z.pow_add_r Z.pow_twice_r using lia : pull_Zpow.
 Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : push_Zmul.
 Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul.
+Hint Rewrite Z.div_div using lia : pull_Zdiv.
+Hint Rewrite <- Z.div_div using lia : push_Zdiv.
 Hint Rewrite <- Z.mul_mod Z.add_mod Zminus_mod using lia : pull_Zmod.
 Hint Rewrite Zminus_mod_idemp_l Zminus_mod_idemp_r : pull_Zmod.