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