proposition: Proposition simple_odd_regular_pgroup_cyclic gT p (H R : {group gT}) : p.-group R -> odd #|R| -> H :!=: 1 -> R \subset 'N(H) -> semiregular H R -> cyclic R.
proof: Proof. move=> pR oddR ntH nHR regR; rewrite (odd_pgroup_rank1_cyclic pR oddR) leqNgt. apply: contra ntH => /p_rank_geP[E /pnElemP[sER abelE dimE2]]. have ncycE: ~~ cyclic E by rewrite (abelem_cyclic abelE) dimE2. have nHE := subset_trans sER nHR. have coHE := coprimegS sER (regular_norm_coprime nHR regR). rewrite -subG1 -(coprime_abelian_gen_cent1 _ _ nHE) ?(abelem_abelian abelE) //. rewrite -bigprodGE big1 // => x; case/setD1P=> nt_x Ex; apply: val_inj => /=. by rewrite regR // !inE nt_x (subsetP sER). 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)