proposition: Lemma FiniteT_nat_cardinal_cond: forall (X:Type) (H:FiniteT X) (n:nat), cardinal (@Full_set X) n -> FiniteT_nat_cardinal X H = n.
proof: Proof. intros. pose proof (FiniteT_has_nat_cardinal X H). destruct H1. red in H1. destruct H1. transitivity x. - symmetry; apply H2. apply FiniteT_nat_cardinal_def. - apply H2; trivial. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)