proposition: Lemma abelian_nil G : abelian G -> nilpotent G.
proof: Proof. by move=> abG; apply/lcnP; exists 1%N; apply/commG1P. 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)