apply toNat_le_of_leNat
p : Nat → Bool
h✝ : ∃ n, p n = true
x : Nat
hlt : x < (first p).toNat ⋯
h : p x = true
⊢ (first p).toNat ⋯ ≤ x
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