proposition: Theorem bounded_search m (P : nat -> Type) : (forall n, n < m -> P n + (P n -> False)) -> { n : nat & (n < m) * P n }%type + { forall n, n < m -> P n -> False }.
proof: Proof. revert P; induction m as [ | m IHm ]; intros P HP. + right; intros; lia. + destruct (HP 0) as [ H0 | H0 ]; try lia. * left; exists 0; split; auto; lia. * destruct IHm with (P := fun n => P (S n)) as [ (n & H1 & H2) | H1 ]. - intros; apply HP; lia. - left; exists (S n); split; auto; lia. - right; intros [ | n ] Hn; auto. apply H1; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)