proposition: Lemma lcnS n A B : A \subset B -> 'L_n(A) \subset 'L_n(B).
proof: Proof. by case: n => // n sAB; elim: n => // n IHn; rewrite !lcnSn genS ?imset2S. 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)