diff options
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. |