fact: Fixpoint nat_bounded_forall (f : nat -> bool) (n : nat) : bool := match n with | O => f n | S n' => andb (f (S n')) (nat_bounded_forall f n') end.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)