proposition: Lemma setIX (A B : finType) (E E' : {set A}) (F F' : {set B}) : E `* F :&: E' `* F' = (E :&: E') `* (F :&: F').
proof: Proof. apply/setP => -[a b]; rewrite !inE /= !andbA; congr (_ && _). by rewrite -!andbA; congr (_ && _); rewrite andbC. Qed.
imports: mathcomp(all_ssreflect fingroup perm)