apply Nat.not_le.2 hlt
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ False
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).toNat ⋯ ≤ x