proposition: Lemma cyclic_center_factor_abelian G : cyclic (G / 'Z(G)) -> abelian G.
proof: Proof. case/cyclicP=> a Ga; case: (cosetP a) => /= z Nz def_a. have G_Zz: G :=: 'Z(G) * <[z]>. rewrite -quotientK ?cycle_subG ?quotient_cycle //=. by rewrite -def_a -Ga quotientGK // center_normal. rewrite G_Zz abelianM cycle_abelian center_abelian centsC /= G_Zz. by rewrite subIset ?centS ?orbT ?mulG_subr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)