diff options
author | Jason Gross <jagro@google.com> | 2018-08-13 18:46:52 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-08-13 18:46:52 -0400 |
commit | c22b3c9726aa1c052fd44bcaf0ced8fb30970206 (patch) | |
tree | 4937a0d4d71ba5d3bdffb4dd16341a83917f6182 /src/Util/ZUtil/Modulo.v | |
parent | cd24907d7c46ddc52989a5cfa7a10c3c4568eee3 (diff) |
Fix split_bounds, prove it correct
Diffstat (limited to 'src/Util/ZUtil/Modulo.v')
-rw-r--r-- | src/Util/ZUtil/Modulo.v | 5 |
1 files changed, 5 insertions, 0 deletions
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. |