From c22b3c9726aa1c052fd44bcaf0ced8fb30970206 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 13 Aug 2018 18:46:52 -0400
Subject: Fix split_bounds, prove it correct

---
 src/Util/ZUtil/Div.v    | 4 ++++
 src/Util/ZUtil/Modulo.v | 5 +++++
 2 files changed, 9 insertions(+)

(limited to 'src/Util/ZUtil')

diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v
index a9fc4aae0..5ae17ad1a 100644
--- a/src/Util/ZUtil/Div.v
+++ b/src/Util/ZUtil/Div.v
@@ -258,4 +258,8 @@ Module Z.
     intros; subst; auto with zarith.
   Qed.
   Hint Resolve div_same' : zarith.
+
+  Lemma div_opp_r a b : a / (-b) = ((-a) / b).
+  Proof. Z.div_mod_to_quot_rem; nia. Qed.
+  Hint Resolve div_opp_r : zarith.
 End Z.
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index 8dea71870..84917a454 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -4,6 +4,7 @@ Require Import Crypto.Util.ZUtil.ZSimplify.Core.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
+Require Import Crypto.Util.ZUtil.Div.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Local Open Scope Z_scope.
@@ -282,4 +283,8 @@ Module Z.
     autorewrite with zsimplify_const.
     reflexivity.
   Qed.
+
+  Lemma mod_opp_r a b : a mod (-b) = -((-a) mod b).
+  Proof. pose proof (Z.div_opp_r a b); Z.div_mod_to_quot_rem; nia. Qed.
+  Hint Resolve mod_opp_r : zarith.
 End Z.
-- 
cgit v1.2.3