proposition: Theorem abelian_structure G : abelian G -> {b | \big[dprod/1]_(x <- b) <[x]> = G & map order b = abelian_type G}.
proof: Proof. rewrite /abelian_type genGidG; have [n] := ubnPleq #|G|. elim: n G => /= [|n IHn] G leGn cGG; first by rewrite leqNgt cardG_gt0 in leGn. rewrite [in _ && _]cGG /=; case: ifP => [ntG|/eqP->]; last first. by exists [::]; rewrite ?big_nil. case: (abelian_type_subproof G) => H /= [//|x ox xdefG]; rewrite -ox. have [_ defG cxH tixH] := dprodP xdefG. have sHG: H \subset G by rewrite -defG mulG_subr. case/IHn: (abelianS sHG cGG) => [|b defH <-]. rewrite -ltnS (leq_trans _ leGn) // -defG TI_cardMg // -orderE. rewrite ltn_Pmull ?cardG_gt0 // ltn_neqAle order_gt0 eq_sym -dvdn1. by rewrite ox -trivg_exponent ntG. by exists (x :: b); rewrite // big_cons defH xdefG. 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)