proposition: Lemma nil_class3 G : (nil_class G <= 3) = ('L_3(G) \subset 'Z(G)).
proof: Proof. rewrite subsetI lcn_sub; apply/idP/commG1P=> [clG3 | L4G1]. by apply/(lcn_nil_classP 3); rewrite ?small_nil_class ?(leq_trans clG3). by apply/(lcn_nil_classP 3) => //; apply/lcnP; exists 3. 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)