proposition: Lemma nat_bounded_forall_char' (f : nat -> bool) (n : nat) : nat_bounded_forall f n = false -> (forall k : nat, k < n -> nat_bounded_forall f k = true) -> forall n' : nat, nat_bounded_forall f n' = (n' <? n).
proof: Proof. intros. induction n. - simpl in *. apply nat_bounded_forall_char; auto. intros. inversion H1. - simpl in *. rewrite Bool.andb_false_iff in H. destruct H. + apply nat_bounded_forall_char; auto. intros. specialize (H0 _ H1). apply nat_bounded_forall_true. assumption. + intuition. destruct (n' <? S n) eqn:?. * apply H0. apply Nat.ltb_lt. assumption. * assert (forall k, k < n -> nat_bounded_forall f k = true). { intros. apply H0. auto. } intuition. rewrite H3. destruct (n' <? n) eqn:?; auto. exfalso. rewrite Nat.ltb_lt in Heqb0. rewrite Nat.ltb_ge in Heqb. rewrite Nat.le_succ_l in Heqb. apply Nat.lt_asymm in Heqb0. contradiction. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)