proposition: Remark prod_sigma_decomposition x : \prod_(x_sM in sigma_decomposition x) x_sM = x.
proof: Proof. rewrite -big_filter; case: big_enumP => /= e _ [Ue De] _; move: De Ue. elim: {x}e (x) => [|y e IHe] x def_e /= Ue. by rewrite big_nil (ell_sigma0P x _) //; apply/pred0P; apply: fsym. have{Ue} [not_e_y Ue] := andP Ue. have [nty] := setD1P (etrans (fsym def_e y) (mem_head _ _)). case/imsetP=> M maxM def_y; rewrite big_cons -(consttC \sigma(M) x) -def_y. congr (y * _); apply: IHe Ue => z; rewrite sigma_decomposition_constt' //. rewrite -def_y inE -def_e !inE andb_orr andNb andb_idl //. by apply: contraTneq => ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)