From e2356788cd28d5ed41b0439573a24f81876daaee Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 15 Jan 2025 16:38:10 -0500
Subject: [PATCH] List/Theory: add decidable_exists_bounded_nat

---
 theories/Spaces/List/Theory.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/Spaces/List/Theory.v b/theories/Spaces/List/Theory.v
index 902fddad19..6c350e4d8d 100644
--- a/theories/Spaces/List/Theory.v
+++ b/theories/Spaces/List/Theory.v
@@ -1249,3 +1249,8 @@ Proof.
   1: exact H1.
   exact _.
 Defined.
+
+Definition decidable_exists_bounded_nat (n : nat) (P : nat -> Type)
+  (H2 : forall k, Decidable (P k))
+  : Decidable { k : nat & prod (k < n) (P k) }
+  := decidable_exists_nat n _ (fun k => fst) _.