fact: Definition N_equiv (p q : N_infty) := forall n, proj1_sig p n = proj1_sig q n.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)