proposition: Theorem bounded_min_d n : (forall x, x < n -> P x \/ Q x) -> (exists x, x < n /\ P x /\ forall y, y < x -> Q y) \/ forall x, x < n -> Q x.
proof: Proof. induction n as [ | n IHn ]; intros Hn. + right; intros; lia. + destruct IHn as [ (x & H1 & H2 & H3) | H1 ]. * intros; apply Hn; lia. * left; exists x; msplit 2; auto; lia. * destruct (Hn n); auto. - left; exists n; msplit 2; auto. - right; intros x Hx. destruct (eq_nat_dec x n); subst; auto. apply H1; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list utils_nat)