diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-18 21:20:54 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-18 21:20:54 -0400 |
| commit | c2436f0f5b314c4765b4087ebe6d2001d459b402 (patch) | |
| tree | 36b5c1439fe101fc2113b68172d3b8695b23af64 /src/Util/ZUtil/Tactics/ZeroBounds.v | |
| parent | 6f9a2b0e28c9511712489929c88c4e9717aee8de (diff) | |
Stronger zero_bounds
Diffstat (limited to 'src/Util/ZUtil/Tactics/ZeroBounds.v')
| -rw-r--r-- | src/Util/ZUtil/Tactics/ZeroBounds.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Tactics/ZeroBounds.v b/src/Util/ZUtil/Tactics/ZeroBounds.v index d10b6714c..86501d84b 100644 --- a/src/Util/ZUtil/Tactics/ZeroBounds.v +++ b/src/Util/ZUtil/Tactics/ZeroBounds.v @@ -1,5 +1,6 @@ Require Import Coq.ZArith.ZArith Coq.omega.Omega. Require Import Crypto.Util.ZUtil.Tactics.PrimeBound. +Require Import Crypto.Util.ZUtil.Div. Local Open Scope Z_scope. Module Z. @@ -9,7 +10,7 @@ Module Z. | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg | [ |- 0 <= _ - _] => apply Z.le_0_sub | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg - | [ |- 0 <= _ / _] => apply Z.div_pos + | [ |- 0 <= _ / _] => apply Z.div_nonneg | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg | [ |- 0 <= _ mod _] => apply Z.mod_pos_bound |