apply first_leNat_of
case h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).leNat x = true
case h.h
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ p x = true