diff options
Diffstat (limited to 'src/Util/ZRange/BasicLemmas.v')
| -rw-r--r-- | src/Util/ZRange/BasicLemmas.v | 3 |
1 files changed, 3 insertions, 0 deletions
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). |