diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-09 13:11:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-09 13:11:02 -0400 |
| commit | 4928c550da6360a7091714bec01af850f00d0072 (patch) | |
| tree | b0d2aeecc82e133ad13a2acdb260df3aa83110e8 /src/Util/ZUtil.v | |
| parent | 77d2f8e3d5c64f08098328306ba7ca42ef8fa321 (diff) | |
Add sub_le_flip_le_Proper
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 83fe2d493..ef4be9e64 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -268,6 +268,8 @@ Module Z. Proof. repeat (omega || intro). Qed. Lemma sub_le_ge_Proper : Proper (Z.le ==> Z.ge ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. + Lemma sub_le_flip_le_Proper : Proper (Z.le ==> Basics.flip Z.le ==> Z.le) Z.sub. + Proof. repeat (omega || intro). Qed. Lemma sub_le_eq_Proper : Proper (Z.le ==> Logic.eq ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. Lemma log2_up_le_Proper : Proper (Z.le ==> Z.le) Z.log2_up. @@ -282,6 +284,8 @@ Module Z. Proof. unfold Basics.flip; repeat (omega || intro). Qed. Lemma sub_le_ge_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.ge ==> Basics.flip Z.le) Z.sub. Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Lemma sub_flip_le_le_Proper_flip : Proper (Basics.flip Z.le ==> Z.le ==> Basics.flip Z.le) Z.sub. + Proof. unfold Basics.flip; repeat (omega || intro). Qed. Lemma sub_le_eq_Proper_flip : Proper (Basics.flip Z.le ==> Logic.eq ==> Basics.flip Z.le) Z.sub. Proof. unfold Basics.flip; repeat (omega || intro). Qed. Lemma log2_up_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le) Z.log2_up. |