diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-02 15:37:37 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-02 15:37:37 -0400 |
| commit | aff1a6e1e6c364515ea804946b2611d99d20d948 (patch) | |
| tree | 11366d3493488b44015ef6626289a968716e247a /src/Util/ZUtil.v | |
| parent | 47c1c427ca53ab6844b49a03cff6ee265cad90f7 (diff) | |
Add ZUtil.Z.log2_ones_lt_nonneg
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index dc8572a8e..47c98d8f9 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2097,6 +2097,12 @@ Module Z. Qed. Hint Resolve log2_ones_le : zarith. + Lemma log2_ones_lt_nonneg x y : 0 < y -> x <= y -> Z.log2 (Z.ones x) < y. + Proof. + rewrite log2_ones_full; apply Z.max_case_strong; omega. + Qed. + Hint Resolve log2_ones_lt_nonneg : zarith. + Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y. Proof. lia. Qed. Hint Rewrite simplify_twice_sub_sub : zsimplify. |