proposition: Theorem bounded_choose_d n : (forall x, x < n -> P x \/ Q x) -> (exists x, x < n /\ P x) \/ forall x, x < n -> Q x.
proof: Proof. intros H. destruct list_choose_d with (P := P) (Q := Q) (l := list_an 0 n) as [ (x & H1 & H2) | H1 ]. + intro; rewrite list_an_spec; intro; apply H; lia. + left; exists x; split; auto. apply list_an_spec in H1; lia. + right; intros x Hx; apply H1, list_an_spec; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list utils_nat)