proposition: Lemma prod_of_disjoint A C x: disjoint_psupports A -> C \in A -> x \in psupport C -> (\prod_(C0 in A) C0) x = C x.
proof: Proof. Proof using. move=> Hdisj HC Hx. have {Hx} Hnotin : {in A :\ C, forall C0 : {perm T}, x \notin psupport C0}. move: Hdisj => [/trivIsetP Hdisj Hinj] C0. rewrite 2!inE => /andP[HC0 HC0A]. move/(_ _ _ (imset_f _ HC) (imset_f _ HC0A)): Hdisj. have Hdiff: psupport C != psupport C0. by apply/contra: HC0 => /eqP/Hinj ->. move=> /(_ Hdiff) /disjoint_setI0 /setP /(_ x). by rewrite inE in_set0 => /nandP[] // /negbTE; rewrite Hx. have Hin : forall i : {perm T}, (i \in A) && (i != C) -> i \in <<A>>. by move => c /andP[Hi _]; apply: mem_gen. have abel := abelian_disjoint_psupports Hdisj. rewrite [X in fun_of_perm X](_ : _ = val (\sum_(C0 in A) fmod abel C0)%R); first last. rewrite -morph_prod /=; last by move=> i; apply: mem_gen. rewrite -[LHS](fmodK abel) //. by apply group_prod => i; apply: mem_gen. rewrite (bigD1 C) //= GRing.addrC -morph_prod //=. rewrite -fmodM /=; [ | exact: group_prod | exact: mem_gen]. rewrite fmodK; last by apply groupM; [exact: group_prod | exact: mem_gen]. rewrite {abel Hin Hdisj HC} permM; congr fun_of_perm. apply big_rec; first by rewrite perm1. move=> i S Hi {2}<-; rewrite permM; congr fun_of_perm. apply/eqP; rewrite -[_ == _]negbK -in_psupport. by apply Hnotin; rewrite !inE andbC. 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