proposition: Lemma cyclic_factor_abelian H G : H \subset 'Z(G) -> cyclic (G / H) -> abelian G.
proof: Proof. move=> sHZ cycGH; apply: cyclic_center_factor_abelian. have /andP[_ nHG]: H <| G := sub_center_normal sHZ. have [f <-]:= homgP (homg_quotientS nHG (gFnorm _ G) sHZ). exact: morphim_cyclic cycGH. 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)