proposition: Lemma disjoint_psupport_dprodE (S : {set {perm T}}) : disjoint_psupports S -> (\big[dprod/1]_(s in S) <[s]>) = (\prod_(s in S) <[s]>)%G.
proof: Proof. Proof using. move=> [/trivIsetP Htriv Hinj]; apply/eqP/bigdprodYP => /= s Hs. apply/subsetP => t; rewrite !inE negb_and negbK. rewrite bigprodGEgen => /gen_prodgP[n [/= f Hf ->{t}]]. apply/andP; split. - case: (altP eqP) => //=; apply contra => Hin. rewrite psupport_eq0 -subset0; apply/subsetP => x Hx. have [i Hxf] : exists i : 'I_n, x \in psupport (f i). apply/existsP; move: Hx; apply contraLR => /=. rewrite negb_exists => /forallP /= Hall; rewrite in_psupport negbK. apply big_rec => [ | i rec _ Hrec]; first by rewrite perm1. by have := Hall i; rewrite permM in_psupport negbK => /eqP ->. move/(_ i): Hf => /bigcupP[/= t /andP[tinS tneqs]]. rewrite inE => /eqP Hfi; rewrite {}Hfi in Hxf. move: Hin Hx => /cycleP[j ->{f}] /(subsetP (psupport_expg _ _)) Hxs. suff : [disjoint psupport t & psupport s]. by rewrite -setI_eq0 => /eqP/setP/(_ x) <-; rewrite inE Hxf Hxs. apply Htriv; try exact: imset_f. by move: tneqs; apply contra => /eqP/Hinj ->. - apply group_prod => i _. have:= Hf i => /bigcupP[/= t /andP[tinS sneqt]]. rewrite inE cent_cycle => /eqP -> {i f Hf}. apply/cent1P; apply: psupport_disjointC. apply Htriv; try exact: imset_f. by move: sneqt; apply contra => /eqP/Hinj ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype