proposition: Lemma nil_class2 G : (nil_class G <= 2) = (G^`(1) \subset 'Z(G)).
proof: Proof. rewrite subsetI der_sub; apply/idP/commG1P=> [clG2 | L3G1]. by apply/(lcn_nil_classP 2); rewrite ?small_nil_class ?(leq_trans clG2). by apply/(lcn_nil_classP 2) => //; apply/lcnP; exists 2. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)