proposition: Remark smallestExists : forall P : nat -> Prop, (forall x : nat, decidable (P x)) -> forall c : nat, P c -> exists a : nat, P a /\ (forall b : nat, b < a -> ~ P b).
proof: Proof. assert (H: forall P : nat -> Prop, (forall x : nat, decidable (P x)) -> forall d c : nat, c < d -> P c -> exists a : nat, P a /\ (forall b : nat, b < a -> ~ P b)). { intros P H d. induction d as [| d Hrecd]. - intros c H0 H1. lia. - intros c H0 H1. assert (H2: c < d \/ c = d) by lia. destruct H2. + eauto. + destruct (boundedCheck P H c). * exists c. tauto. * destruct H3 as (x, H3). apply (Hrecd x). -- lia. -- tauto. } intros P H0 c H1. eapply H. - exact H0. - exact (Nat.lt_succ_diag_r c). - exact H1. Qed.