proposition: Lemma cyclic_nilpotent_quo_der1_cyclic G : nilpotent G -> cyclic (G / G^`(1)) -> cyclic G.
proof: Proof. move=> nG; rewrite (isog_cyclic (quotient1_isog G)). have [-> // | ntG' cGG'] := (eqVneq G^`(1) 1)%g. suffices: 'L_2(G) \subset G :&: 'L_3(G) by move/(eqfun_inP nG)=> <-. rewrite subsetI lcn_sub /= -quotient_cents2 ?lcn_norm //. apply: cyclic_factor_abelian (lcn_central 2 G) _. by rewrite (isog_cyclic (third_isog _ _ _)) ?lcn_normal // lcn_subS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)