diff options
Diffstat (limited to 'src/Util/ZRange/BasicLemmas.v')
| -rw-r--r-- | src/Util/ZRange/BasicLemmas.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 8da5e69d7..6b5a430c4 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -8,6 +8,7 @@ Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Tactics.DestructHead. @@ -97,4 +98,12 @@ Module ZRange. intros; Bool.split_andb; rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; cbn [lower upper] in *; split_min_max. all: lia. Qed. + + Lemma is_bounded_by_bool_opp x r : is_bounded_by_bool (Z.opp x) (ZRange.opp r) = is_bounded_by_bool x r. + Proof. + cbv [is_bounded_by_bool andb opp]; cbn [lower upper]; break_match; Z.ltb_to_lt; break_match; Z.ltb_to_lt; + try (symmetry; progress Z.ltb_to_lt); + try reflexivity; + try lia. + Qed. End ZRange. |