proposition: Lemma nil_class_quotient_center G : nilpotent (G) -> nil_class (G / 'Z(G)) = (nil_class G).-1.
proof: Proof. move=> nilG; have nsZ1G := ucn_normal 1 G. apply/eqP; rewrite -ucn1 eqn_leq; apply/andP; split. apply/ucn_nil_classP; rewrite ?quotient_nil //= -quotient_ucn_add ucn1. by rewrite (ucn_nil_classP _ _ _) ?addn1 ?leqSpred. rewrite -subn1 leq_subLR addnC; apply/ucn_nil_classP => //=. apply: (quotient_inj _ nsZ1G) => /=. by apply: normalS (ucn_sub _ _) nsZ1G; rewrite /= addnS ucn_sub_geq. by rewrite quotient_ucn_add; apply/ucn_nil_classP; rewrite //= quotient_nil. 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)