From bcd99195575ca1c45d49c21a46b9caaecd9bbc10 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 Jul 2016 11:44:29 -0700 Subject: Add more ZUtil lemmas We really want rewrite mod AC here... --- src/Util/ZUtil.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src') 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. -- cgit v1.2.3