From 39a7ef1f4787381bf7013025cae1d8edc980500c Mon Sep 17 00:00:00 2001
From: Jade Philipoom <jadep@google.com>
Date: Thu, 8 Mar 2018 16:11:06 +0100
Subject: move some lemmas to ZUtil/ListUtil

---
 src/Util/ZUtil/Div.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/Util/ZUtil')

diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v
index d660a9935..c596dbab3 100644
--- a/src/Util/ZUtil/Div.v
+++ b/src/Util/ZUtil/Div.v
@@ -124,6 +124,9 @@ Module Z.
   Qed.
   Hint Rewrite div_add_exact using zutil_arith : zsimplify.
 
+  Lemma Z_divide_div_mul_exact' a b c : b <> 0 -> (b | a) -> a * c / b = c * (a / b).
+  Proof. intros. rewrite Z.mul_comm. auto using Z.divide_div_mul_exact. Qed.
+
   Lemma div_sub_mod_exact a b : b <> 0 -> a / b = (a - a mod b) / b.
   Proof.
     intro.
-- 
cgit v1.2.3