proposition: Lemma N_infty_false_eq_nat_inj : forall p : N_infty, forall n : nat, (proj1_sig p) n = false -> { n' | p = nat_inj n' }.
proof: Proof. intros. destruct (N_infty_false_eq_nat_inj' _ _ H) as [n']. exists n'. auto using N_infty_extensionality. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)