proposition: Lemma powersetI A B : powerset (A :&: B) = powerset A :&: powerset B.
proof: Proof. by apply/setP=> C; rewrite !inE subsetI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)