proposition: Lemma porbit_set_of_disjoint A : disjoint_psupports A -> porbit_set (\prod_(C0 in A) C0) = \bigcup_(C0 in A) porbit_set C0.
proof: Proof. Proof using. move=> Hdisj; apply/setP => X; rewrite inE. apply/andP/bigcupP => [[]/imsetP[x _ ->]/[dup]Hcard | [C] HC]. - rewrite psupport_card_porbit psupport_of_disjoint //. move=> /bigcupP => [][C HC Hx]; exists C => //. rewrite inE; apply/andP; split => //. apply/imsetP; exists x => //. apply/setP => y. by apply/porbitP/porbitP =>[][i ->]; exists i; rewrite (expg_prod_of_disjoint _ _ HC). - rewrite inE => /andP[/imsetP[x _ ->] Hcard]. split => //. apply/imsetP; exists x => //. apply/setP=> y; rewrite psupport_card_porbit in Hcard. by apply/porbitP/porbitP =>[][i ->]; exists i; rewrite (expg_prod_of_disjoint _ _ HC). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp