diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-02 15:21:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-02 15:22:01 -0400 |
| commit | d6e3cc2cf525aa42efe4e55c632c1afc466652e8 (patch) | |
| tree | 5c0984d32c51cf57cd3f9fd62d0f5c2b078dc698 /src/Util/ZUtil.v | |
| parent | 2a60b05e1cc80732b2e6958fb5b5cfb621c7087f (diff) | |
Add ZUtil lemma
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c133f1f8a..79067ac9d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2065,6 +2065,13 @@ Module Z. Qed. Hint Rewrite log2_pred_pow2_full : zsimplify. + Lemma ones_lt_pow2 x y : 0 <= x <= y -> Z.ones x < 2^y. + Proof. + rewrite Z.ones_equiv, Z.lt_pred_le. + auto with zarith. + Qed. + Hint Resolve ones_lt_pow2 : zarith. + Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y. Proof. lia. Qed. Hint Rewrite simplify_twice_sub_sub : zsimplify. |