proposition: Lemma size_abelian_type G : abelian G -> size (abelian_type G) = 'r(G).
proof: Proof. move=> cGG; have [b defG def_t] := abelian_structure cGG. apply/eqP; rewrite -def_t size_map eqn_leq andbC; apply/andP; split. have [p p_pr ->] := rank_witness G; rewrite p_rank_abelian //. by rewrite -indexg1 -(Ohm0 G) -(count_logn_dprod_cycle _ _ defG) count_size. case/lastP def_b: b => // [b' x]; pose p := pdiv #[x]. have p_pr: prime p. have:= abelian_type_gt1 G; rewrite -def_t def_b map_rcons -cats1 all_cat. by rewrite /= andbT => /andP[_]; apply: pdiv_prime. suffices: all [pred y | logn p #[y] > 0] b. rewrite all_count (count_logn_dprod_cycle _ _ defG) -def_b; move/eqP <-. by rewrite Ohm0 indexg1 -p_rank_abelian ?p_rank_le_rank. apply/allP=> y; rewrite def_b mem_rcons inE /= => b_y. rewrite lognE p_pr order_gt0 (dvdn_trans (pdiv_dvd _)) //. case/predU1P: b_y => [-> // | b'_y]. have:= abelian_type_dvdn_sorted G; rewrite -def_t def_b. case/splitPr: b'_y => b1 b2; rewrite -cat_rcons rcons_cat map_cat !map_rcons. rewrite headI /= cat_path -(last_cons 2) -headI last_rcons. case/andP=> _ /order_path_min min_y. apply: (allP (min_y _)) => [? ? ? ? dv|]; first exact: (dvdn_trans dv). by rewrite mem_rcons mem_head. 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)