proposition: Remark sigma_cover_decomposition x x' : \ell_\sigma(x) == 1%N -> x' \in 'R[x] -> sigma_decomposition (x * x') = x |: [set x']^#.
proof: Proof. move=> ell1x Rx'; have [-> | ntx'] := eqVneq x' 1. by rewrite mulg1 setDv setU0 ell1_decomposition. rewrite setDE (setIidPl _) ?sub1set ?inE // setUC. have ntR: #|'R[x]| > 1 by rewrite cardG_gt1; apply/trivgPn; exists x'. have [Ns_x' cxx'] := setIP Rx'; move/cent1P in cxx'. have [[_ <- _ _] [//| maxN _ t2Nx _ _]] := FT_signalizer_context ell1x. have{maxN} [maxN _] := mem_uniq_mmax maxN. have sNx' := mem_p_elt (pcore_pgroup _ _) Ns_x'. have sN'x: \sigma('N[x])^'.-elt x by apply: sub_p_elt t2Nx => p /andP[]. have defx': (x * x').`_\sigma('N[x]) = x'. by rewrite consttM // (constt1P sN'x) mul1g constt_p_elt. have sd_xx'_x': x' \in sigma_decomposition (x * x'). by rewrite 2!inE ntx' -{1}defx'; apply: imset_f. rewrite -(setD1K sd_xx'_x') -{3}defx' -sigma_decomposition_constt' ?consttM //. by rewrite constt_p_elt // (constt1P _) ?p_eltNK ?mulg1 // ell1_decomposition. 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)