proposition: Lemma ucn_lcnP n G : ('L_n.+1(G) == 1) = ('Z_n(G) == G).
proof: Proof. rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G); set i := (n in LHS). have: i + 0 = n by [rewrite addn0]; elim: i 0 => [j <- //|i IHi j]. rewrite addSnnS => /IHi <- {IHi}; rewrite ucnSn lcnSn. rewrite -sub_morphim_pre ?gFsub_trans ?gFnorm_trans // subsetI. by rewrite morphimS ?gFsub // quotient_cents2 ?gFsub_trans ?gFnorm_trans. 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)