have : (first p).leNat (bfind p h) := by
  unfold bfind
  rw [leNat_toNat]
p : Nat → Bool
h : ∃ n, p n = true
⊢ p (bfind p h) = true
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
⊢ p (bfind p h) = true