proposition: Lemma grank_abelian G : abelian G -> 'm(G) = 'r(G).
proof: Proof. move=> cGG; apply/eqP; rewrite eqn_leq; apply/andP; split. rewrite -size_abelian_type //; case/abelian_structure: cGG => b defG <-. suffices <-: <<[set x in b]>> = G. by rewrite (leq_trans (grank_min _)) // size_map cardsE card_size. rewrite -{G defG}(bigdprodWY defG). elim: b => [|x b IHb]; first by rewrite big_nil gen0. by rewrite big_cons -joingE -joing_idr -IHb joing_idl joing_idr set_cons. have [p p_pr ->] := rank_witness G; pose K := 'Mho^1(G). have ->: 'r_p(G) = logn p #|G / K|. rewrite p_rank_abelian // card_quotient /= ?gFnorm // -divgS ?Mho_sub //. by rewrite -(mul_card_Ohm_Mho_abelian 1 cGG) mulnK ?cardG_gt0. case: (grank_witness G) => B genB <-; rewrite -genB. have{genB}: <<B>> \subset G by rewrite genB. have [m] := ubnP #|B|; elim: m B => // m IHm B. have [-> | [x Bx]] := set_0Vmem B; first by rewrite gen0 quotient1 cards1 logn1. rewrite ltnS (cardsD1 x) Bx -[in <<B>>](setD1K Bx); set B' := B :\ x => ltB'm. rewrite -joingE -joing_idl -joing_idr -/<[x]> join_subG => /andP[Gx sB'G]. rewrite cent_joinEl ?(sub_abelian_cent2 cGG) //. have nKx: x \in 'N(K) by rewrite -cycle_subG (subset_trans Gx) ?gFnorm. rewrite quotientMl ?cycle_subG // quotient_cycle //= -/K. have le_Kxp_1: logn p #[coset K x] <= 1. rewrite -(dvdn_Pexp2l _ _ (prime_gt1 p_pr)) -p_part -order_constt. rewrite order_dvdn -morph_constt // -morphX ?groupX //= coset_id //. by rewrite Mho_p_elt ?p_elt_constt ?groupX -?cycle_subG. apply: leq_trans (leq_add le_Kxp_1 (IHm _ ltB'm sB'G)). by rewrite -lognM ?dvdn_leq_log ?muln_gt0 ?cardG_gt0 // mul_cardG dvdn_mulr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)