proposition: Lemma setP_finite E : finite_set E -> finite_set (\Po E).
proof: Proof. move => /NatP h. rewrite /finite_set card_setP; apply/NatP; rewrite - cpowcr; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)