proposition: Fact bounded_search_ni n : (forall i, i < n -> P i \/ ~ P i) -> (forall i, i < n -> ~ P i) \/ exists i, i < n /\ P i /\ forall j, j < i -> ~ P j.
proof: Proof. revert P; induction n as [ | n IHn ]; intros P HP. + left; intros; lia. + destruct (HP 0) as [ H | H ]; try lia. - right; exists 0; split; try lia; split; auto; intros; lia. - destruct IHn with (P := fun n => P (S n)) as [ H1 | (x & H1 & H2 & H3) ]. * intros; apply HP; lia. * left; intros [] ?; auto; apply H1; lia. * right; exists (S x); split; try lia; split; auto. intros [] ?; auto; apply H3; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)