proposition: Lemma infinite_powerset E: infinite_set E -> infinite_set (\Po E).
proof: Proof. move=> /infinite_setP iE; move: (proj1 (cantor (CS_cardinal E))) => lt1. apply/infinite_setP; rewrite card_setP - cpowcr. apply: (cle_inf_inf iE lt1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)