proposition: Lemma FiniteT_nat_cardinal_bijection: forall (X Y:Type) (H:FiniteT X) (g:X->Y) (Hinv:invertible g), FiniteT_nat_cardinal Y (bij_finite X Y g H Hinv) = FiniteT_nat_cardinal X H.
proof: Proof. intros. apply FiniteT_nat_cardinal_cond. apply invertible_impl_bijective in Hinv. destruct Hinv as [g_inj g_surj]. rewrite Im_Full_set_surj in g_surj. rewrite g_surj. apply injection_preserves_cardinal; trivial. apply FiniteT_nat_cardinal_def. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)