proposition: Lemma disjoint_psupports_cycles A : {in A, forall C, C \is cyclic} -> disjoint_psupports A -> {in A, forall C, psupport C \in porbits (\prod_(C in A) C)}.
proof: Proof. Proof using. move=> Hcycle Hdisj C HC; move/(_ C HC): Hcycle. rewrite /cyclic => /cards1P[X] Hpsupp. have:= eq_refl X; rewrite -in_set1 -Hpsupp inE => /andP[/imsetP[x _] Hx]. subst X; rewrite porbitE=> Hcard. have:= cover_partition (partition_psupport C); rewrite Hpsupp. rewrite /cover big_set1 => <-; apply/imsetP; exists x => //. have Hx : x \in psupport C. rewrite in_psupport; apply/eqP; rewrite -apermE => /afix1P. rewrite -afix_cycle => /orbit1P Hcontra. by move: Hcard; rewrite Hcontra cards1. by apply/setP => y; apply/porbitP/porbitP => [] [i] ->; exists i; apply esym; rewrite (expg_prod_of_disjoint i Hdisj 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