Finding iteration satisfying a predicate in option if exists

Stream: Is there code for X?

[Naruyoko]

Suppose I have the following:

• f : S → option S, which satisfies that for all x : S, there is some n such that (λ x, x >>= f)^[n] $ some x = none, so iteration is finite.
• A decidable predicate P on S, maybe as P : set S with decidable_pred P.

Then, how can I concisely write 1) the finiteness of iteration of f, and 2) the function S → option S such that:
a) If there is some k such that (λ x, x >>= f)^[k] $ some x = some z and z ∈ P, then return (λ x, x >>= f)^[k₀] $ some x where k₀ is minimum such k
b) Otherwise, return none.

In particular, I want to make such a function when S = ℕ and f x = none or f x = some z where z < x.

[Yakov Pechersky]

Express it as a existential, and pass it to docs#Nat.find

[Yakov Pechersky]

For the first half. For the second half, wrap the call to Nat.find in a dependent if.