Add some minor reflect things

2 files changed, 5 insertions, 0 deletions

diff --git a/src/Util/Bool/Reflect.v b/src/Util/Bool/Reflect.v
index d9e93fe93..8a5333f0a 100644
--- a/src/Util/Bool/Reflect.v
+++ b/src/Util/Bool/Reflect.v
@@ -69,6 +69,7 @@ Ltac beq_to_eq beq bl lb :=
 Existing Class reflect.
 Definition decb (P : Prop) {b : bool} {H : reflect P b} := b.
 Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)).
+Definition decb_rel {A B} (P : A -> B -> Prop) {b : A -> B -> bool} {H : reflect_rel P b} := b.
 
 Lemma decb_true_iff P {b} {H : reflect P b} : @decb P b H = true <-> P.
 Proof. symmetry; apply reflect_iff, H. Qed.
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v
index ae3c71ef4..0258e5c8e 100644
--- a/src/Util/ZRange.v
+++ b/src/Util/ZRange.v
@@ -2,6 +2,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Bool.Reflect.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Notations.
 
@@ -98,6 +99,9 @@ Proof.
   subst; split; reflexivity.
 Qed.
 
+Global Instance reflect_zrange_eq : reflect_rel (@eq zrange) zrange_beq | 10.
+Proof. apply reflect_of_beq; auto using zrange_bl, zrange_lb. Qed.
+
 Global Instance zrange_rect_Proper {P}
   : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq) (@zrange_rect (fun _ => P)) | 10.
 Proof.