proposition: Lemma FiniteT_cardinality {X : Type} : FiniteT X <-> lt_cardinal X nat.
proof: Proof. split; intros. - constructor. + destruct (FiniteT_nat_embeds H) as [f]. exists f. assumption. + intros [f []]. apply nat_infinite. apply surj_finite with (f := f); auto. intros; apply classic. - destruct H as [[f Hf] H]. apply NNPP. intro. destruct (infinite_nat_inj _ H0) as [g]. contradict H. apply CSB with (f := f) (g := g); auto. Qed.
imports: Coq(ClassicalChoice) Coq(ProofIrrelevance) Coq(FunctionalExtensionality) Coq(Description) ZornsLemma(FunctionPropertiesEns) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(CSB) ZornsLemma(EnsemblesSpec) ZornsLemma(ZornsLemma) ZornsLemma(EnsemblesImplicit) ZornsLemma(CountableTypes) ZornsLemma(FiniteTypes) ZornsLemma(InfiniteTypes) Coq(RelationClasses)