For decidable D and a witness i<N with D(i), construct least r<N with D(r) and all k<r satisfying not D(k).
Method: native-induction. Induction: N. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.