proposition: Proposition 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. have actsR: {acts R, on group H | 'J} by split; rewrite ?subsetT ?astabsJ. apply: ext_odd_regular_pgroup_cyclic pR oddR ntH actsR _ => // x Rx. by rewrite gacentJ cent_set1 regR. 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)