proposition: Lemma bounded_min (P : nat -> Prop) : (forall x, P x \/ ~ P x) -> forall n, (exists k, k < n /\ P k /\ forall i, i < k -> ~ P i) \/ forall k, k < n -> ~ P k.
proof: Proof. intros HP. induction n as [ | n IHn ]. + right; intros; lia. + destruct IHn as [ (k & H1 & H2 & H3) | H ]. * left; exists k; repeat split; auto; lia. * destruct (HP n). - left; exists n; repeat split; auto. - right; intros k Hk. destruct (eq_nat_dec k n); subst; auto. apply H; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)