diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-09 17:02:38 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-09 17:02:38 -0400 |
| commit | f731a49d3d79e63f986ab73f2198051c3ada0c76 (patch) | |
| tree | d870a8c8cda18435a767166ade689062ec57bdd8 /src/Util/ZUtil.v | |
| parent | 411934edebbc26dbdf9bd45ae8a4afccb5dbae23 (diff) | |
Add Z.lt_le_flip_Proper_flip_impl
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 39e2c8abb..03b9e0e56 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -279,6 +279,9 @@ Module Z. Proof. intros ???; apply Z.log2_le_mono; assumption. Qed. Lemma pow_Zpos_le_Proper x : Proper (Z.le ==> Z.le) (Z.pow (Z.pos x)). Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. + Lemma lt_le_flip_Proper_flip_impl + : Proper (Z.le ==> Basics.flip Z.le ==> Basics.flip Basics.impl) Z.lt. + Proof. unfold Basics.flip; repeat (omega || intro). Qed. Lemma le_Proper_ge_le_flip_impl : Proper (Z.le ==> Z.ge ==> Basics.flip Basics.impl) Z.le. Proof. intros ???????; omega. Qed. Lemma add_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le ==> Basics.flip Z.le) Z.add. |