proposition: Fact first_which_ni : (exists x, P x) -> exists m, P m /\ forall x, x < m -> ~ P x.
proof: Proof. Proof using HP. intros (n & Hn). destruct (@bounded_search_ni (S n)) as [ H1 | (m & H1 & H2 & H3) ]. + intros; auto. + contradict Hn; apply H1; lia. + exists m; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)