proposition: Lemma odd_pgroup_rank1_cyclic gT p (G : {group gT}) : p.-group G -> odd #|G| -> cyclic G = ('r_p(G) <= 1).
proof: Proof. move=> pG oddG; rewrite -rank_pgroup //; apply/idP/idP=> [cycG | dimG1]. by rewrite -abelian_rank1_cyclic ?cyclic_abelian. have [X nsXG cXX|//|] := normal_rank1_structure pG; last first. by rewrite (negPf (odd_not_extremal2 oddG)) andbF. by rewrite abelian_rank1_cyclic // (leq_trans (rankS (normal_sub nsXG))). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal)