proposition: Lemma card_uniq P : finite P -> exists! n, exists (f : N n -> elts P), bijective f.
proof: Proof. intros [n [f [f_inj f_surj]]]. ex n. split. ex f. fo. intros m [g [g_inj g_surj]]. apply Nat.le_antisymm. apply N_inj_le with (f := inverse g_surj o f). inj. apply N_inj_le with (f := inverse f_surj o g). inj. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)