proposition: Lemma trivg_center_pgroup P : p.-group P -> 'Z(P) = 1 -> P :=: 1.
proof: Proof. move=> pP Z1; apply/eqP/idPn=> ntP. have{ntP} [p_pr p_dv_P _] := pgroup_pdiv pP ntP. suff: p %| #|'Z(P)| by rewrite Z1 cards1 gtnNdvd ?prime_gt1. by rewrite /center /dvdn -afixJ -pgroup_fix_mod // astabsJ normG. 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)