apply bfind_le_of_prop
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ find p h ≤ x
case h
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ ∃ n, decide (p n) = true

case a
p : Nat → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
x : Nat
hx : p x
⊢ decide (p x) = true