proposition: Lemma sigma_cover_disjoint x y : \ell_\sigma(x) == 1%N -> \ell_\sigma(y) == 1%N -> x != y -> [disjoint x *: 'R[x] & y *: 'R[y]].
proof: Proof. move=> ell1x ell1y neq_xy; apply/pred0P=> g /=. have [[ntx _] [nty _]] := (ell_sigma1P x ell1x, ell_sigma1P y ell1y). apply: contraNF (ntx) => /andP[/lcosetP[x' Rxx' ->{g}] /= yRy_xx']. have def_y: y = x'. apply: contraTeq (mem_sigma_cover_decomposition ell1y yRy_xx') => neq_yx'. by rewrite sigma_cover_decomposition // !inE negb_or nty eq_sym neq_xy. have [[_ <- _ _] [|uniqCx _ _ _ _]] := FT_signalizer_context ell1x. by rewrite cardG_gt1; apply/trivgPn; exists x'; rewrite // -def_y. have{uniqCx} [maxNx sCxNx] := mem_uniq_mmax uniqCx. have Rx_y: y \in 'R[x] by [rewrite def_y]; have [Nxs_y cxy] := setIP Rx_y. have Ry_x: x \in 'R[y]. by rewrite -def_y -(cent1P cxy) mem_lcoset mulKg in yRy_xx'. have MSyNx: 'N[x] \in 'M_\sigma[y] by rewrite inE maxNx cycle_subG. have [[_ <- _ _] [|uniqCy _ _ _]] := FT_signalizer_context ell1y. by rewrite cardG_gt1; apply/trivgPn; exists x. have{uniqCy} [_ sCyNy] := mem_uniq_mmax uniqCy. case/(_ 'N[x] MSyNx)=> /sdprodP[_ _ _ tiRyNx] _ _ _. rewrite -in_set1 -set1gE -tiRyNx -setIA (setIidPr sCyNy) inE Ry_x /=. by rewrite inE cent1C cxy (subsetP sCxNx) ?cent1id. 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)