theorem PGroups.p_group_center_nontrivial {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [Finite G] (hG : IsPGroup p G) [Nontrivial G] : Nontrivial ↥(Subgroup.center G)