proposition: Lemma nat_bounded_forall_lt (f : nat -> bool) (n m : nat) : nat_bounded_forall f n = true -> m < n -> nat_bounded_forall f m = true.
proof: Proof. intros. induction n. { inversion H0. } simpl in *. apply andb_prop in H. intuition. inversion H0; subst; auto. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)