diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-25 13:37:16 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-25 13:37:16 -0500 |
| commit | 1f954745f214b82cbd6c79e61f89a966d463da8e (patch) | |
| tree | b81c84bc454cb4d0cb9040a93f0329e7b6304459 /src/Util | |
| parent | 0803746ae4cc556e06e3ba5fadb98bbbcbf638ab (diff) | |
Move le_{add,sub}_1_* to ZUtil.Le
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ZUtil/Le.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Le.v b/src/Util/ZUtil/Le.v index ca180c556..a32d0fdd0 100644 --- a/src/Util/ZUtil/Le.v +++ b/src/Util/ZUtil/Le.v @@ -55,4 +55,10 @@ Module Z. Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. Proof. lia. Qed. + + Lemma le_sub_1_iff x y : x <= y - 1 <-> x < y. + Proof. lia. Qed. + + Lemma le_add_1_iff x y : x + 1 <= y <-> x < y. + Proof. lia. Qed. End Z. |