proposition: Lemma nat_unbounded_impl_countably_infinite (U : Ensemble nat) (HU : forall n : nat, exists m : nat, In U m /\ n < m) : eq_cardinal_ens U (@Full_set nat).
proof: Proof. apply nat_unbounded_impl_countably_infinite_dec; auto. intros ?. apply classic. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)