proposition: Lemma minimize (P : nat -> Prop) : (forall x, P x \/ ~ P x) -> (exists n, P n) -> exists n, P n /\ forall i, i < n -> ~ P i.
proof: Proof. intros HP (n & Hn). destruct (@bounded_min _ HP (S n)) as [ (k & H1 & H2 & H3) | H ]. + exists k; split; auto. + exfalso; apply H with n; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)