proposition: Proposition coprime_abelian_gen_cent1 gT (A G : {group gT}) : abelian A -> ~~ cyclic A -> A \subset 'N(G) -> coprime #|G| #|A| -> <<\bigcup_(a in A^#) 'C_G[a]>> = G.
proof: Proof. move=> abelA ncycA nGA coGA. apply/eqP; rewrite eq_sym eqEsubset /= gen_subG. apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl. rewrite -{1}(coprime_abelian_gen_cent abelA nGA) ?genS //. apply/bigcupsP=> B; have [-> | /trivgPn[a Ba n1a]] := eqsVneq B 1. by rewrite injm_cyclic ?coset1_injm ?norms1 ?(negbTE ncycA). case/and3P=> _ sBA _; rewrite (bigcup_max a) ?inE ?n1a ?(subsetP sBA) //. by rewrite setIS // -cent_set1 centS // sub1set. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)