proposition: Lemma eqcard_equipotent (aT rT: finType): (#|aT| = #|rT|) <-> (exists f : aT -> rT, bijective f).
proof: Proof. split. move => sc. move:(enum_val_bij aT) => []; set n1 := #|_ |; move => g1 c1 c2. move:(enum_val_bij rT) => []; set n2 := #|_ |; move => g2 c3 c4. have nn: n1 = n2 by rewrite /n1 /n2. exists (fun x => enum_val (cast_ord nn (g1 x))). exists (fun x => enum_val (cast_ord (sym_eq nn) (g2 x))). by move => t /=;rewrite c3 cast_ord_comp cast_ord_id c2. by move => t /=; rewrite c1 cast_ord_comp cast_ord_id c4. move => [f bf]. have rtb: {on rT, bijective f} by apply: onW_bij. rewrite -(on_card_preimset rtb) - cardsT. have -> // : f @^-1: rT = [set: aT] by apply/setP=> x; rewrite !inE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)