proposition: Lemma nil_Zgroup_cyclic G : Zgroup G -> nilpotent G -> cyclic G.
proof: Proof. have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn ZgG nilG. have [->|[p pr_p pG]] := trivgVpdiv G; first by rewrite -cycle1 cycle_cyclic. have /dprodP[_ defG Cpp' _] := nilpotent_pcoreC p nilG. have /cyclicP[x def_p]: cyclic 'O_p(G). have:= forallP ZgG 'O_p(G)%G. by rewrite (p_Sylow (nilpotent_pcore_Hall p nilG)). have /cyclicP[x' def_p']: cyclic 'O_p^'(G). have sp'G := pcore_sub p^' G. apply: IHn (leq_trans _ leGn) (ZgroupS sp'G _) (nilpotentS sp'G _) => //. rewrite proper_card // properEneq sp'G andbT; case: eqP => //= def_p'. by have:= pcore_pgroup p^' G; rewrite def_p' /pgroup p'natE ?pG. apply/cyclicP; exists (x * x'); rewrite -{}defG def_p def_p' cycleM //. by red; rewrite -(centsP Cpp') // (def_p, def_p') cycle_id. by rewrite /order -def_p -def_p' (@pnat_coprime p) //; apply: pcore_pgroup. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)