proposition: Lemma CountableT_is_FiniteT_or_countably_infinite (X : Type) : CountableT X -> {FiniteT X} + {exists f : X -> nat, bijective f}.
proof: Proof. intros. apply exclusive_dec. - intro. destruct H0 as [? [f ?]]. contradiction nat_infinite. apply bij_finite with _ f; trivial. apply bijective_impl_invertible; trivial. - destruct (classic (FiniteT X)). + left; trivial. + right. apply infinite_nat_inj in H0. destruct H as [f], H0 as [g]. now apply CSB with f g. Qed.
imports: Coq(Arith ArithRing ClassicalChoice Description FunctionalExtensionality Lia Relation_Definitions Program.Subset QArith ZArith) ZornsLemma(CSB DecidableDec DependentTypeChoice Finite_sets FiniteTypes FunctionPropertiesEns IndexedFamilies InfiniteTypes)