proposition: Lemma lcn_subS n G : 'L_n.+1(G) \subset 'L_n(G).
proof: Proof. case: n => // n; rewrite lcnSn commGC commg_subr. by case/andP: (lcn_normal n.+1 G). 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)