proposition: Lemma cent_classP x G : reflect (x ^: G = [set x]) (x \in 'C(G)).
proof: Proof. apply: (iffP (centP _ _)) => [Cx | Cx1 y Gy]. apply/eqP; rewrite eqEsubset sub1set class_refl andbT. by apply/subsetP=> _ /imsetP[y Gy ->]; rewrite !inE conjgE Cx ?mulKg. by apply/commgP/conjg_fixP/set1P; rewrite -Cx1; apply/imsetP; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)