diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-08 13:10:35 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-08 13:10:35 -0500 |
| commit | b103fcc6f1d130cc4c6d9200851f62a392c1d798 (patch) | |
| tree | af025f9d535ab908e10abae60e789444f23a2f78 /src/Util/ZUtil.v | |
| parent | c89a77f3b6de068aaf1b8cd2adad73ef64c7fb13 (diff) | |
Prove things in ModularBaseSystemListZOperationsProofs
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 17e8d62bf..9dc4eeb51 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -944,6 +944,7 @@ Module Z. rewrite Z.ones_succ by assumption. zero_bounds. Qed. + Hint Resolve ones_nonneg : zarith. Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. Proof. @@ -953,6 +954,7 @@ Module Z. apply Z.lt_succ_lt_pred. apply Z.pow_gt_1; omega. Qed. + Hint Resolve ones_pos_pos : zarith. Lemma pow2_mod_id_iff : forall a n, 0 <= n -> (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n). |