proposition: Remark ell_sigma1P x : reflect (x != 1 /\ 'M_\sigma[x] != set0) (\ell_\sigma(x) == 1%N).
proof: Proof. apply: (iffP idP) => [ell1x | [ntx]]; last first. case/set0Pn=> M /setIdP[maxM]; rewrite cycle_subG => Ms_x. by rewrite (Msigma_ell1 maxM) // in_setD1 ntx. have sdx_x: x \in sigma_decomposition x by rewrite ell1_decomposition ?set11. have{sdx_x} [ntx sdx_x] := setD1P sdx_x; split=> //; apply/set0Pn. have{sdx_x} [M maxM def_x] := imsetP sdx_x; rewrite // -cycle_eq1 in ntx. have sMx: \sigma(M).-elt x by rewrite def_x p_elt_constt. have [[z sXzMs] _] := sigma_Jsub maxM sMx ntx. by exists (M :^ z^-1)%G; rewrite inE mmaxJ maxM MsigmaJ -sub_conjg. 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)