Add more ZUtil lemmas

We really want rewrite mod AC here...

1 files changed, 14 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 9bd134f10..a1d53f02b 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -647,6 +647,20 @@ Module Z.
     rewrite div_mul_diff_exact by assumption; lia.
   Qed.
 
+  Lemma div_mul_diff_exact'' a b c
+        (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c)
+    : a * c / b = (a / b) * c + (c * (a mod b)) / b.
+  Proof.
+    rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia.
+  Qed.
+
+  Lemma div_mul_diff_exact''' a b c
+        (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c)
+    : (a / b) * c = a * c / b - (c * (a mod b)) / b.
+  Proof.
+    rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia.
+  Qed.
+
   Lemma div_mul_diff a b c
         (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c)
     : c * a / b - c * (a / b) <= c.