proposition: Lemma setX0 (A B : finType) (E : {set A}) : E `* set0 = set0 :> {set A * B}.
proof: Proof. apply/setP/subset_eqP/andP; split; apply/subsetP => -[a b]; rewrite !inE //. by move/andP => []. Qed.
imports: mathcomp(all_ssreflect fingroup perm)