diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-11 19:05:46 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-11 19:05:46 -0500 |
| commit | ce4e7ace7826be7d6b28a299f2060021f0cf699f (patch) | |
| tree | a7e11ad69d75b369fbd338b8771b9f1d8b67adcc /src/Util/ZRange/BasicLemmas.v | |
| parent | 340daa051b413c0ae154de2bbe242e931a57f8c6 (diff) | |
Add ZRange.normalize_constant
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). |