proposition: Lemma lcn_norm n G : G \subset 'N('L_n(G)).
proof: Proof. exact/char_norm/lcn_char. 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)