apply not_prop_of_lt_bfind hlt
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ False
case a
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
h : p x = true
hlt : x < bfind p h✝
⊢ p x = true