proposition: Fact first_which : (exists x, P x) -> { m | P m /\ forall x, x < m -> ~ P x }.
proof: Proof. Proof using HP. intros H. destruct (min_dec H) as (m & H1 & H2). exists m; split; auto. intros x Hx H3. apply H2 in H3. lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)