proposition: Lemma card_powerset (T : finType) (A : {set T}) : #|powerset A| = 2 ^ #|A|.
proof: Proof. rewrite -card_bool -(card_pffun_on false) -(card_imset _ val_inj). apply: eq_card => f; pose sf := false.-support f; pose D := finset sf. have sDA: (D \subset A) = (sf \subset A) by apply: eq_subset; apply: in_set. have eq_sf x : sf x = f x by rewrite /= negb_eqb addbF. have valD: val D = f by rewrite /D unlock; apply/ffunP=> x; rewrite ffunE eq_sf. apply/imsetP/pffun_onP=> [[B] | [sBA _]]; last by exists D; rewrite // inE ?sDA. by rewrite inE -sDA -valD => sBA /val_inj->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)