More zarith

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
2m59.90s | Total                                           | 2m45.43s || +0m14.46s
----------------------------------------------------------------------------------
0m47.27s | ModularArithmetic/Pow2BaseProofs                | 0m37.78s || +0m09.49s
0m11.27s | ModularArithmetic/Montgomery/ZProofs            | 0m09.44s || +0m01.83s
0m17.72s | ModularArithmetic/ModularBaseSystemProofs       | 0m17.72s || +0m00.00s
0m13.74s | Experiments/SpecEd25519                         | 0m13.85s || -0m00.10s
0m12.31s | Specific/GF25519                                | 0m12.16s || +0m00.15s
0m11.55s | Util/ZUtil                                      | 0m11.60s || -0m00.04s
0m09.67s | Testbit                                         | 0m08.91s || +0m00.75s
0m07.47s | Specific/GF1305                                 | 0m07.60s || -0m00.12s
0m05.37s | BaseSystemProofs                                | 0m04.60s || +0m00.77s
0m04.17s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m03.98s || +0m00.18s
0m03.70s | ModularArithmetic/Tutorial                      | 0m03.70s || +0m00.00s
0m03.48s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m04.13s || -0m00.64s
0m03.32s | Experiments/SpecificCurve25519                  | 0m03.34s || -0m00.02s
0m03.12s | ModularArithmetic/ModularArithmeticTheorems     | 0m03.00s || +0m00.12s
0m02.55s | ModularArithmetic/BarrettReduction/ZBounded     | 0m02.37s || +0m00.17s
0m02.41s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.36s || +0m00.05s
0m02.08s | ModularArithmetic/BarrettReduction/Z            | 0m02.06s || +0m00.02s
0m01.97s | Encoding/PointEncodingPre                       | 0m01.68s || +0m00.29s
0m01.66s | BaseSystem                                      | 0m01.26s || +0m00.39s
0m01.55s | ModularArithmetic/PrimeFieldTheorems            | 0m01.17s || +0m00.38s
0m01.40s | Experiments/DerivationsOptionRectLetInEncoding  | 0m01.25s || +0m00.14s
0m01.28s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.83s || +0m00.45s
0m01.21s | ModularArithmetic/ExtendedBaseVector            | 0m01.15s || +0m00.06s
0m01.00s | Util/NumTheoryUtil                              | 0m00.88s || +0m00.12s
0m00.98s | ModularArithmetic/Montgomery/ZBounded           | 0m00.97s || +0m00.01s
0m00.75s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.71s || +0m00.04s
0m00.70s | Encoding/ModularWordEncodingPre                 | 0m00.65s || +0m00.04s
0m00.69s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.78s || -0m00.09s
0m00.68s | Encoding/ModularWordEncodingTheorems            | 0m01.00s || -0m00.31s
0m00.66s | ModularArithmetic/ModularBaseSystemList         | 0m00.67s || -0m00.01s
0m00.64s | ModularArithmetic/ModularBaseSystem             | 0m00.61s || +0m00.03s
0m00.63s | ModularArithmetic/ZBounded                      | 0m00.44s || +0m00.19s
0m00.60s | ModularArithmetic/Montgomery/Z                  | 0m00.50s || +0m00.09s
0m00.57s | Spec/ModularWordEncoding                        | 0m00.57s || +0m00.00s
0m00.50s | ModularArithmetic/Pre                           | 0m00.52s || -0m00.02s
0m00.46s | ModularArithmetic/Pow2Base                      | 0m00.43s || +0m00.03s
0m00.40s | Spec/ModularArithmetic                          | 0m00.36s || +0m00.04s
0m00.38s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.41s || -0m00.02s

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 35aa20dc4..1758f1496 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -19,7 +19,7 @@ Hint Extern 1 => lia : lia.
 Hint Extern 1 => lra : lra.
 Hint Extern 1 => nia : nia.
 Hint Extern 1 => omega : omega.
-Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound : zarith.
+Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg Z.lt_le_incl Z.pow_nonzero Z.div_le_upper_bound Z_div_exact_full_2 Z.div_same Z.div_lt_upper_bound Z.div_le_lower_bound Zplus_minus Zplus_gt_compat_l Zplus_gt_compat_r Zmult_gt_compat_l Zmult_gt_compat_r Z.pow_lt_mono_r Z.pow_lt_mono_l Z.pow_lt_mono Z.mul_lt_mono_nonneg Z.div_lt_upper_bound Z.div_pos : zarith.
 Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) (fun a b pf => proj1 (Z.pow_gt_1 a b pf)) : zarith.
 
 Ltac zutil_arith := solve [ omega | lia | auto with nocore ].