proposition: Lemma lcnSnS n G : [~: 'L_n(G), G] \subset 'L_n.+1(G).
proof: Proof. by case: n => //; apply: der1_subG. 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)