Add more ZUtil lemmas

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
1m48.08s | Total                                           | 1m41.98s || +0m06.09s
----------------------------------------------------------------------------------
0m33.64s | Specific/GF25519                                | 0m32.52s || +0m01.11s
0m15.92s | ModularArithmetic/ModularBaseSystemProofs       | 0m15.19s || +0m00.73s
0m11.47s | Experiments/SpecEd25519                         | 0m11.25s || +0m00.22s
0m07.31s | Specific/GF1305                                 | 0m07.11s || +0m00.19s
0m04.46s | ModularArithmetic/Pow2BaseProofs                | 0m03.86s || +0m00.60s
0m04.12s | ModularArithmetic/Tutorial                      | 0m03.87s || +0m00.25s
0m03.90s | BaseSystemProofs                                | 0m03.70s || +0m00.19s
0m03.22s | ModularArithmetic/ModularBaseSystemOpt          | 0m03.15s || +0m00.07s
0m02.75s | Util/ZUtil                                      | 0m02.71s || +0m00.04s
0m01.66s | ModularArithmetic/ModularArithmeticTheorems     | 0m01.63s || +0m00.03s
0m01.59s | ModularArithmetic/PrimeFieldTheorems            | 0m01.54s || +0m00.05s
0m01.55s | Encoding/PointEncodingPre                       | 0m01.47s || +0m00.08s
0m01.49s | ModularArithmetic/BarrettReduction/Z            | 0m00.97s || +0m00.52s
0m01.24s | BaseSystem                                      | 0m01.16s || +0m00.08s
0m01.20s | Util/NumTheoryUtil                              | 0m00.86s || +0m00.34s
0m01.11s | ModularArithmetic/ExtendedBaseVector            | 0m01.13s || -0m00.01s
0m00.99s | Encoding/ModularWordEncodingTheorems            | 0m00.72s || +0m00.27s
0m00.98s | Experiments/DerivationsOptionRectLetInEncoding  | 0m00.94s || +0m00.04s
0m00.95s | Encoding/ModularWordEncodingPre                 | 0m00.61s || +0m00.34s
0m00.91s | ModularArithmetic/ModularBaseSystemField        | 0m00.88s || +0m00.03s
0m00.89s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.62s || +0m00.27s
0m00.85s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.80s || +0m00.04s
0m00.75s | Experiments/SpecificCurve25519                  | 0m00.74s || +0m00.01s
0m00.68s | ModularArithmetic/ModularBaseSystem             | 0m00.56s || +0m00.12s
0m00.68s | Testbit                                         | 0m00.63s || +0m00.05s
0m00.63s | Spec/ModularWordEncoding                        | 0m00.61s || +0m00.02s
0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.58s || +0m00.03s
0m00.59s | ModularArithmetic/ModularBaseSystemList         | 0m00.59s || +0m00.00s
0m00.59s | ModularArithmetic/Pre                           | 0m00.42s || +0m00.17s
0m00.56s | ModularArithmetic/Pow2Base                      | 0m00.39s || +0m00.17s
0m00.44s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.43s || +0m00.01s
0m00.35s | Spec/ModularArithmetic                          | 0m00.35s || +0m00.00s

1 files changed, 25 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 1a7b54d84..1e0ed36e4 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1235,6 +1235,31 @@ Module Z.
   Proof. lia. Qed.
   Hint Rewrite simplify_twice_sub_add : zsimplify.
 
+  Lemma simplify_once_add_add_add x y z : x + y + (x + z) = 2 * x + y + z.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_add_add_add : zsimplify.
+  Lemma simplify_once_add_add_sub x y z : x + y + (x - z) = 2 * x + y - z.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_add_add_sub : zsimplify.
+  Lemma simplify_once_add_sub_add x y z : x + y - (x + z) = y - z.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_add_sub_add : zsimplify.
+  Lemma simplify_once_add_sub_sub x y z : x + y - (x - z) = y + z.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_add_sub_sub : zsimplify.
+  Lemma simplify_once_sub_add_add x y z : x - y + (x + z) = 2 * x - y + z.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_sub_add_add : zsimplify.
+  Lemma simplify_once_sub_add_sub x y z : x - y + (x - z) = 2 * x - y - z.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_sub_add_sub : zsimplify.
+  Lemma simplify_once_sub_sub_add x y z : x - y - (x + z) = -y - z.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_sub_sub_add : zsimplify.
+  Lemma simplify_once_sub_sub_sub x y z : x - y - (x - z) = z - y.
+  Proof. lia. Qed.
+  Hint Rewrite simplify_once_sub_sub_sub : zsimplify.
+
   Section equiv_modulo.
     Context (N : Z).
     Definition equiv_modulo x y := x mod N = y mod N.