proposition: Lemma card_powerset_rw x y: cardinal x = cardinal y -> cardinal (\Po x) = cardinal (\Po y).
proof: Proof. by move => eq; rewrite ! card_setP - cpowcr eq cpowcr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)