proposition: Lemma prime_odd_regular_normal gT (H R P : {group gT}) : prime #|P| -> odd #|R| -> P \subset R -> H :!=: 1 -> R \subset 'N(H) -> semiregular H R -> P <| R.
proof: Proof. set p := #|P| => pr_p oddR sPR ntH nHR regHR. have pP: p.-group P := pnat_id pr_p. have cycQ (q : nat) (Q : {group gT}) : q.-group Q -> Q \subset R -> cyclic Q. move=> qQ sQR; have [oddQ nHQ] := (oddSg sQR oddR, subset_trans sQR nHR). exact: odd_regular_pgroup_cyclic qQ oddQ ntH nHQ (semiregularS _ sQR regHR). have cycRq (q : nat): cyclic 'O_q(R) by rewrite (cycQ q) ?pcore_pgroup ?gFsub. suffices cFP: P \subset 'C('F(R)). have nilF: nilpotent 'F(R) := Fitting_nil R. have hallRp: p.-Hall('F(R)) 'O_p('F(R)) := nilpotent_pcore_Hall p nilF. apply: char_normal_trans (pcore_normal p R); rewrite sub_cyclic_char //=. rewrite -p_core_Fitting (sub_normal_Hall hallRp) ?gFnormal //. have solR: solvable R. by apply: metacyclic_sol; apply: odd_regular_metacyclic regHR. by apply: subset_trans (cent_sub_Fitting solR); rewrite subsetI sPR. rewrite centsC -(bigdprodWY (erefl 'F(R))) gen_subG big_tnth. apply/bigcupsP=> i _; move: {i}(tuple.tnth _ i) => q. have [<- | q'p] := eqVneq p q. have [Q sylQ sPQ] := Sylow_superset sPR pP; have [sQR pQ _] := and3P sylQ. rewrite (sub_abelian_cent2 (cyclic_abelian (cycQ _ _ pQ sQR))) //. by rewrite pcore_sub_Hall. have [-> | ntRq] := eqVneq 'O_q(R) 1%g; first exact: sub1G. have /andP[sRqR qRq]: q.-subgroup(R) 'O_q(R) by apply: pcore_psubgroup. have [pr_q _ _] := pgroup_pdiv qRq ntRq. have coRqP: coprime #|'O_q(R)| p by rewrite (pnat_coprime qRq) // pnatE. have nRqP: P \subset 'N('O_q(R)) by rewrite (subset_trans sPR) ?gFnorm. rewrite centsC (coprime_odd_faithful_Ohm1 qRq) ?(oddSg sRqR) //. apply: sub_abelian_cent2 (joing_subl _ _) (joing_subr _ _) => /=. set PQ := P <*> _; have oPQ: #|PQ| = (p * q)%N. rewrite /PQ norm_joinEl 1?gFnorm_trans //. rewrite coprime_cardMg 1?coprime_sym ?(coprimeSg (Ohm_sub 1 _)) // -/p. by congr (p * _)%N; apply: Ohm1_cyclic_pgroup_prime => /=. have sPQ_R: PQ \subset R by rewrite join_subG sPR (subset_trans (Ohm_sub 1 _)). have nH_PQ := subset_trans sPQ_R nHR. apply: cyclic_abelian; apply: regular_pq_group_cyclic oPQ ntH nH_PQ _ => //. exact: semiregularS regHR. 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)