proposition: Lemma N_infty_false_minimal : forall p : N_infty, forall n : nat, (proj1_sig p) n = false -> { n' : nat | (proj1_sig p) n' = false /\ forall k, k < n' -> (proj1_sig p) k = true }.
proof: Proof. intros. induction n. - exists 0; intuition. inversion H0. - destruct (proj1_sig p n) eqn:?. + exists (S n); intuition. destruct (Nat.eq_dec k n). * subst. assumption. * apply (proj2_sig p n); auto. rewrite Nat.lt_succ_r in H0. induction H0; try contradiction. rewrite Nat.lt_succ_r. assumption. + apply IHn. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)