proposition: Lemma Puig1 G : 'L_{1}(G) = G.
proof: Proof. apply/eqP; rewrite eqEsubset Puig_at_sub; apply/subsetP=> x Gx. rewrite -cycle_subG sub_gen // -[<[x]>]/(gval _) bigcup_sup //=. by rewrite inE cycle_subG Gx /= /norm_abelian cycle_abelian sub1G. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)