proposition: Corollary FiniteT_has_nat_cardinal (X : Type) : FiniteT X -> exists! n:nat, cardinal (@Full_set X) n.
proof: Proof. intros. apply -> unique_existence; split. - apply FiniteT_has_nat_cardinal'. assumption. - red; intros. apply cardinal_unicity with X Full_set; trivial. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)