proposition: Lemma morphim_lcn n G : G \subset D -> f @* 'L_n(G) = 'L_n(f @* G).
proof: Proof. move=> sHG; case: n => //; elim=> // n IHn. by rewrite !lcnSn -IHn morphimR // (subset_trans _ sHG) // 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)