proposition: Lemma nil_class1 G : (nil_class G <= 1) = abelian G.
proof: Proof. have [-> | ntG] := eqsVneq G 1. by rewrite abelian1 leq_eqVlt ltnS leqn0 nil_class0 eqxx orbT. apply/idP/idP=> cGG. apply/commG1P; apply/(lcn_nil_classP 1); rewrite // nilpotent_class. by rewrite (leq_ltn_trans cGG) // cardG_gt1. by apply/(lcn_nil_classP 1); rewrite ?abelian_nil //; 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)