From a49d6945893959d894795ce4fcbe6f7238a81ee5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Dec 2018 18:33:06 -0500 Subject: Add ZRange.OperationBounds --- src/Util/ZRange/BasicLemmas.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Util/ZRange/BasicLemmas.v') 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. -- cgit v1.2.3