proposition: Lemma Eqc_setX a b a' b': a =c a' -> b =c b' -> (a \times b) =c (a' \times b').
proof: Proof. move => /card_eqP [f [bf <- <-]] /card_eqP [f' [bf' <- <-]]; apply/card_eqP. move:(ext_to_prod_fb bf bf') => h. by exists (f \ftimes f'); split => //; rewrite /ext_to_prod; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)