proposition: Lemma odd_regular_metacyclic gT (H R : {group gT}) : odd #|R| -> H :!=: 1 -> R \subset 'N(H) -> semiregular H R -> metacyclic R.
proof: Proof. move=> oddR ntH nHR regHR. apply/Zgroup_metacyclic/forall_inP=> P /SylowP[p pr_p /and3P[sPR pP _]]. have [oddP nHP] := (oddSg sPR oddR, subset_trans sPR nHR). exact: odd_regular_pgroup_cyclic pP oddP ntH nHP (semiregularS _ sPR 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)