proposition: Lemma lcn_char n G : 'L_n(G) \char G.
proof: Proof. by case: n; last elim=> [|n IHn]; rewrite ?char_refl ?lcnSn ?charR. 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)