proposition: Lemma Frobenius_Wielandt_fixpoint (M : {group gT}) : [Frobenius G = K ><| R] -> G \subset 'N(M) -> coprime #|M| #|G| -> solvable M -> [/\ (#|'C_M(G)| ^ #|R| * #|M| = #|'C_M(R)| ^ #|R| * #|'C_M(K)|)%N, 'C_M(R) = 1 -> K \subset 'C(M) & 'C_M(K) = 1 -> (#|M| = #|'C_M(R)| ^ #|R|)%N].
proof: Proof. move=> frobG nMG coMG solM; have [defG _ ntR _ _] := Frobenius_context frobG. have [_ _ _ _ /eqP snRG] := and5P frobG. have [nsKG sRG _ _ tiKR] := sdprod_context defG; have [sKG _] := andP nsKG. pose m0 (_ : {group gT}) := 0%N. pose Dm := [set 1%G; G]; pose Dn := K |: orbit 'JG K R. pose m := [fun A => 0%N with 1%G |-> #|K|, G |-> 1%N]. pose n A : nat := A \in Dn. have out_m: {in [predC Dm], m =1 m0}. by move=> A; rewrite !inE /=; case/norP; do 2!move/negbTE->. have out_n: {in [predC Dn], n =1 m0}. by rewrite /n => A /=; move/negbTE=> /= ->. have ntG: G != 1%G by case: eqP sRG => // -> <-; rewrite subG1. have neqKR: K \notin orbit 'JG K R. apply/imsetP=> [[x _ defK]]; have:= Frobenius_dvd_ker1 frobG. by rewrite defK cardJg gtnNdvd // ?prednK // -subn1 subn_gt0 cardG_gt1. have Gmn A: m A + n A > 0 -> A \subset G. rewrite /=; case: eqP => [-> | ] _; first by rewrite sub1G. rewrite /n 2!inE; do 2!case: eqP => [-> // | ] _. case R_A: (A \in _) => // _; case/imsetP: R_A => x Kx ->{A}. by rewrite conj_subG ?(subsetP sKG). have partG: {in G, forall a, \sum_(A | a \in gval A) m A = \sum_(A | a \in gval A) n A}%N. - move=> a Ga; have [-> | nt_a] := eqVneq a 1. rewrite (bigD1 1%G) ?inE ?eqxx //= (bigD1 G) ?inE ?group1 //=. rewrite (negbTE ntG) !eqxx big1 ?addn1 => [|A]; last first. by rewrite group1 -negb_or -in_set2; apply: out_m. rewrite (bigID (mem Dn)) /= addnC big1 => [|A]; last first. by rewrite group1; apply: out_n. transitivity #|Dn|. rewrite cardsU1 neqKR card_orbit astab1JG. by rewrite -{3}(setIidPl sKG) -setIA -normD1 snRG tiKR indexg1. by rewrite -sum1_card /n; apply: eq_big => [A | A ->]; rewrite ?group1. rewrite (bigD1 G) //= (negbTE ntG) eqxx big1 => [|A]; last first. case/andP=> Aa neAG; apply: out_m; rewrite !inE; case: eqP => // A1. by rewrite A1 inE (negbTE nt_a) in Aa. have [partG tiG _] := and3P (Frobenius_partition frobG). do [rewrite -(eqP partG); set pG := _ |: _] in Ga tiG. rewrite (bigD1 <<pblock pG a>>%G) /=; last by rewrite mem_gen // mem_pblock. rewrite big1 => [|B]; last first. case/andP=> Ba neqBA; rewrite -/(false : nat); congr (nat_of_bool _). apply: contraTF neqBA; rewrite negbK -val_eqE /=. case/setU1P=> [BK | /imsetP[x Kx defB]]. by rewrite (def_pblock tiG _ Ba) BK ?setU11 ?genGid. have Rxa: a \in R^# :^ x by rewrite conjD1g !inE nt_a -(congr_group defB). rewrite (def_pblock tiG _ Rxa) ?setU1r ?imset_f // conjD1g. by rewrite genD1 ?group1 // genGid defB. rewrite /n !inE -val_eqE /= -/(true : nat); congr ((_ : bool) + _)%N. case/setU1P: (pblock_mem Ga) => [-> |]; first by rewrite genGid eqxx. case/imsetP=> x Kx ->; symmetry; apply/orP; right. apply/imsetP; exists x => //. by apply: val_inj; rewrite conjD1g /= genD1 ?group1 // genGid. move/eqP: (solvable_Wielandt_fixpoint Gmn nMG coMG solM partG). rewrite (bigD1 1%G) // (bigD1 G) //= eqxx (setIidPl (cents1 _)) cards1 muln1. rewrite (negbTE ntG) eqxx mul1n -(sdprod_card defG) (mulnC #|K|) expnM. rewrite mulnA -expnMn big1 ?muln1 => [|A]; last first. by rewrite -negb_or -in_set2; move/out_m; rewrite /m => /= ->. rewrite mulnC eq_sym (bigID (mem Dn)) /= mulnC. rewrite big1 ?mul1n => [|A]; last by move/out_n->. rewrite big_setU1 //= /n setU11 mul1n. rewrite (eq_bigr (fun _ => #|'C_M(R)| ^ #|R|)%N) => [|A R_A]; last first. rewrite inE R_A orbT mul1n; case/imsetP: R_A => x Kx ->. suffices nMx: x \in 'N(M) by rewrite -{1}(normP nMx) centJ -conjIg !cardJg. exact: subsetP (subsetP sKG x Kx). rewrite mulnC prod_nat_const card_orbit astab1JG. have ->: 'N_K(R) = 1 by rewrite -(setIidPl sKG) -setIA -normD1 snRG tiKR. rewrite indexg1 -expnMn eq_sym eqn_exp2r ?cardG_gt0 //; move/eqP=> eq_fix. split=> // [regR | regK]. rewrite centsC (sameP setIidPl eqP) eqEcard subsetIl /=. move: eq_fix; rewrite regR cards1 exp1n mul1n => <-. suffices ->: 'C_M(G) = 1 by rewrite cards1 exp1n mul1n. by apply/trivgP; rewrite -regR setIS ?centS //; case/sdprod_context: defG. move: eq_fix; rewrite regK cards1 muln1 => <-. suffices ->: 'C_M(G) = 1 by rewrite cards1 exp1n mul1n. by apply/trivgP; rewrite -regK setIS ?centS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)