proposition: Lemma disjoint_psupports_porbits A : {in A, forall C, C \is cyclic} -> disjoint_psupports A -> {in porbit_set (\prod_(C in A) C), forall X, exists2 C, C \in A & psupport C = X}.
proof: Proof. Proof using. move=> Hcycle Hdisj X; rewrite inE => /andP[/imsetP[x _ -> {X}] Hcard]. case: (boolP (x \in psupport (\prod_(C in A) C))) => [Hin|]. - have [C0 HC0 Hx] : exists2 C0, (C0 \in A) & (x \in psupport C0). apply/exists_inP. apply/contraLR: Hin; rewrite negb_exists => /forallP Hnotin. rewrite in_psupport negbK; apply/eqP/out_perm_prod => C HC. by have:= Hnotin C; rewrite HC andTb. exists C0 => //; move: Hx. have /imsetP[y _ ->] : psupport C0 \in (porbits (\prod_(C in A) C)). exact: disjoint_psupports_cycles. by rewrite -eq_porbit_mem => /eqP. - rewrite in_psupport negbK porbitE -apermE => /eqP /afix1P. rewrite -afix_cycle => /orbit1P. rewrite -porbitE => Hcontra; move: Hcard. by rewrite Hcontra cards1. 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