proposition: Lemma odd_rank1_Zgroup gT (G : {group gT}) : odd #|G| -> Zgroup G = ('r(G) <= 1).
proof: Proof. move=> oddG; apply/forallP/idP=> [ZgG | rG_1 P]. have [p p_pr ->]:= rank_witness G; have [P sylP]:= Sylow_exists p G. have [sPG pP _] := and3P sylP; have oddP := oddSg sPG oddG. rewrite -(p_rank_Sylow sylP) -(odd_pgroup_rank1_cyclic pP) //. by apply: (implyP (ZgG P)); apply: (p_Sylow sylP). apply/implyP=> /SylowP[p p_pr /and3P[sPG pP _]]. rewrite (odd_pgroup_rank1_cyclic pP (oddSg sPG oddG)). by apply: leq_trans (leq_trans (p_rank_le_rank p G) rG_1); apply: p_rankS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)