From ce4e7ace7826be7d6b28a299f2060021f0cf699f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Dec 2018 19:05:46 -0500 Subject: Add ZRange.normalize_constant --- src/Util/ZRange/BasicLemmas.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Util/ZRange') diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 2fbeb3068..11441225e 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -170,6 +170,9 @@ Module ZRange. cbv [opp upper lower]; destruct r; rewrite !Z.opp_involutive; reflexivity. Qed. + Lemma normalize_constant v : normalize (constant v) = constant v. + Proof. repeat t2_step. Qed. + Lemma is_bounded_by_bool_move_opp_normalize r v : is_bounded_by_bool v (ZRange.normalize (-r)) = is_bounded_by_bool (-v) (ZRange.normalize r). -- cgit v1.2.3