proposition: Lemma lcn_sub_leq m n G : n <= m -> 'L_m(G) \subset 'L_n(G).
proof: Proof. by move/subnK <-; elim: {m}(m - n) => // m; apply: subset_trans (lcn_subS _ _). 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)