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]. assert (Full_set = Im Full_set g). apply Extensionality_Ensembles; split; red; intros; try constructor. destruct (g_surj x). exists x0; try constructor; auto. rewrite H0; apply injection_preserves_cardinal; trivial. apply FiniteT_nat_cardinal_def. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description FunctionalExtensionality