proposition: Remark boundedCheck : forall P : nat -> Prop, (forall x : nat, decidable (P x)) -> forall c : nat, (forall d : nat, d < c -> ~ P d) \/ (exists d : nat, d < c /\ P d).
proof: Proof. intros P H c. induction c as [| c Hrecc]. - left; intros d H0. lia. - destruct (H c) as [e | e]. + right. exists c. split; auto. + destruct Hrecc as [H0 | H0]. * left. intros d H1. assert (d < c \/ d = c) as H2 by lia. destruct H2. -- eauto. -- congruence. * destruct H0 as (x, H0). right. exists x. split; try lia. tauto. Qed.