proposition: Lemma Eqc_setXb x y: fgraphs_equipotent x y -> (productb x) =c (productb y).
proof: Proof. move=> [dxy ale]. pose g i := equipotent_ex (Vg x i) (Vg y i). pose f i := graph (g i). rewrite -(productb_gr x) - (productb_gr y) - dxy. apply/card_eqP;exists (ext_map_prod (domain x) (Vg x) (Vg y) f). hnf; rewrite /ext_map_prod; saw. have ea: ext_map_prod_axioms (domain x) (Vg x) (Vg y) f. move=> i iI; move: (equipotent_ex_pr1 (ale _ iI))=> [[[fg _] _] sg tg]. rewrite /f; split; fprops. by rewrite - sg; apply: domain_fg. by rewrite -tg;apply: f_range_graph. split. apply: ext_map_prod_fi =>// i iI. move: (equipotent_ex_pr1 (ale _ iI)) => /proj31 /proj1. by rewrite -/(g _); move => [ [_ qa qb] qc]; split => //; rewrite - qb. apply: ext_map_prod_fs =>//. move=> i iI; move: (equipotent_ex_pr1 (ale _ iI)) => [[ig sg] _ p4]. by rewrite /f -p4 - (surjective_pr0 sg) (ImfE (proj1 sg)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)