proposition: Remark notBoundedForall : forall (P : nat -> Prop) (b : nat), (forall x : nat, decidable (P x)) -> ~ (forall n : nat, n < b -> P n) -> exists n : nat, n < b /\ ~ P n.
proof: Proof. intros P b H H0; induction b as [| b Hrecb]. - elim H0. lia. - destruct (H b) as [e | e]. + assert (H1: ~ (forall n : nat, n < b -> P n)). { intro H1. elim H0. intros n H2. assert (n < b \/ n = b) as H3 by lia. destruct H3. - auto. - rewrite H3; auto. } decompose record (Hrecb H1) /r; intros x H3 H4. exists x. split; auto; lia. + exists b. split; auto; lia. Qed.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)