proposition: Lemma sigma_decomposition_constt' x M (sM := \sigma(M)) : M \in 'M -> sigma_decomposition x.`_sM^' = sigma_decomposition x :\ x.`_sM.
proof: Proof. move=> maxM; apply/setP=> y; rewrite !inE andbCA; apply: andb_id2l => nty. apply/imsetP/andP=> [ | [neq_y_xM /imsetP]] [L maxL def_y]. have not_sMy: ~~ sM.-elt y. apply: contra nty => sMy; rewrite -order_eq1 (pnat_1 sMy) // def_y. by apply: p_eltX; apply: p_elt_constt. split; first by apply: contraNneq not_sMy => ->; apply: p_elt_constt. have notMGL: gval L \notin M :^: G. apply: contra not_sMy; rewrite def_y; case/imsetP=> z _ ->. by rewrite (eq_constt _ (sigmaJ M z)) p_elt_constt. apply/imsetP; exists L; rewrite // def_y sub_in_constt // => p _ sLp. by apply: contraFN (sigma_partition maxM maxL notMGL p) => sMp; apply/andP. exists L; rewrite ?sub_in_constt // => p _ sLp. suffices notMGL: gval L \notin M :^: G. by apply: contraFN (sigma_partition maxM maxL notMGL p) => sMp; apply/andP. apply: contra neq_y_xM; rewrite def_y => /imsetP[z _ ->]. by rewrite (eq_constt _ (sigmaJ M z)). 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)