proposition: Lemma lcn_normalS n G : 'L_n.+1(G) <| 'L_n(G).
proof: Proof. by apply: normalS (lcn_normal _ _); rewrite (lcn_subS, lcn_sub). 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)