proposition: Lemma card_class_support_sigma M : M \in 'M -> #|class_support M^~~ G| = (#|M`_\sigma|.-1 * #|G : M|)%N.
proof: Proof. move=> maxM; rewrite [#|M`_\sigma|](cardsD1 1) group1 /=. set MsG := class_support (M`_\sigma)^# G; pose P := [set x *: 'R[x] | x in MsG]. have ellMsG x: x \in MsG -> \ell_\sigma(x) == 1%N. by case/imset2P=> y z My _ ->; rewrite ell_sigmaJ (Msigma_ell1 maxM). have tiP: trivIset P. apply/trivIsetP=> _ _ /imsetP[x MsGx ->] /imsetP[y MsGy ->] neq_xRyR. by rewrite sigma_cover_disjoint ?ellMsG //; apply: contraNneq neq_xRyR => ->. have->: class_support M^~~ G = cover P. apply/setP=> az; apply/imset2P/bigcupP=> [[a z] | [xRz]]. case/bigcupP=> x Ms_x xRa Gz ->; exists (x ^ z *: 'R[x ^ z]). by apply: imset_f; apply: imset2_f. by rewrite sigma_coverJ memJ_conjg. case/imsetP=> _ /imset2P[x z Ms_x Gz ->] ->; rewrite sigma_coverJ. by case/imsetP=> a xRa ->; exists a z => //; apply/bigcupP; exists x. rewrite -(eqnP tiP) big_imset /= => [|x y MsGx MsGy eq_xyR]; last first. have: x *: 'R[x] != set0 by rewrite -cards_eq0 -lt0n card_lcoset cardG_gt0. rewrite -[x *: _]setIid {2}eq_xyR setI_eq0. by apply: contraNeq => neq_xy; rewrite sigma_cover_disjoint ?ellMsG. rewrite -{2}(norm_mmax maxM) -astab1JG -indexgI -card_orbit. set MG := orbit _ G M; rewrite mulnC -sum_nat_const. transitivity (\sum_(Mz in MG) \sum_(x in (Mz`_\sigma)^#) 1); last first. apply: eq_bigr => _ /imsetP[z _ ->]; rewrite sum1_card MsigmaJ. by rewrite -conjD1g cardJg. rewrite (exchange_big_dep (mem MsG)) /= => [|Mz xz]; last first. case/imsetP=> z Gz ->; rewrite MsigmaJ -conjD1g => /imsetP[x Ms_x ->{xz}]. exact: imset2_f. apply: eq_bigr => x MsGx; rewrite card_lcoset sum1dep_card. have ell1x := ellMsG x MsGx; have [ntx _] := ell_sigma1P x ell1x. have [[transRx -> _ _] _] := FT_signalizer_context ell1x. apply: eq_card => Mz; rewrite 2!inE cycle_subG in_setD1 ntx /=. apply: andb_id2r => Mzs_x. apply/idP/imsetP=> [maxMz | [z _ ->]]; last by rewrite mmaxJ. have [y t Ms_y _ def_x] := imset2P MsGx; have{Ms_y} [_ Ms_y] := setD1P Ms_y. have [MSxMz MSxMt]: Mz \in 'M_\sigma[x] /\ (M :^ t)%G \in 'M_\sigma[x]. by rewrite {2}def_x cycleJ sigma_mmaxJ inE maxMz inE maxM !cycle_subG. have [z _ ->] := atransP2 transRx MSxMt MSxMz. by exists (t * z); rewrite ?inE ?actM. 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)