diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-11 18:33:06 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-11 18:33:06 -0500 |
| commit | a49d6945893959d894795ce4fcbe6f7238a81ee5 (patch) | |
| tree | d299971aeb82d8700c84ca999c8ca3bd96e6691d /src/Util/ZRange/BasicLemmas.v | |
| parent | 13499c36b211e8346a50c279aef7b35b2bc87833 (diff) | |
Add ZRange.OperationBounds
Diffstat (limited to 'src/Util/ZRange/BasicLemmas.v')
| -rw-r--r-- | src/Util/ZRange/BasicLemmas.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 5f434c771..e41657428 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -177,4 +177,9 @@ Module ZRange. rewrite <- is_bounded_by_bool_opp at 1. rewrite normalize_opp, opp_involutive; reflexivity. Qed. + + Lemma is_tighter_than_bool_constant r v + : is_tighter_than_bool (ZRange.constant v) r + = is_bounded_by_bool v r. + Proof. reflexivity. Qed. End ZRange. |