proposition: Lemma center_nil_eq1 G : nilpotent G -> ('Z(G) == 1) = (G :==: 1).
proof: Proof. move=> nilG; apply/eqP/eqP=> [Z1 | ->]; last exact: center1. by rewrite (TI_center_nil nilG) // (setIidPr (center_sub G)). 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)