proposition: Lemma cprod_inf3 E F: nonempty E -> E <=cc F -> infinite_set F -> (F \times E) =c F.
proof: Proof. move=> /card_nonempty1 neE le1 /infinite_setP infF. by rewrite - cprod2_pr1 - cprod2cl - cprod2cr; apply:cprod_inf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)