proposition: Lemma Exercise6_4a E: infinite_set E -> cardinal (\Po (coarse E)) = cardinal (\Po E).
proof: Proof. move => /infinite_setP ife. apply: (card_powerset_rw). by rewrite /coarse - cprod2_pr1 - cprod2cl - cprod2cr csquare_inf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)