proposition: Lemma cent_semiprime H K X : semiprime K H -> X \subset H -> X :!=: 1 -> 'C_K(X) = 'C_K(H).
proof: Proof. move=> prKH sXH /trivgPn[x Xx ntx]; apply/eqP. rewrite eqEsubset -{1}(prKH x) ?inE ?(subsetP sXH) ?ntx //=. by rewrite -cent_cycle !setIS ?centS ?cycle_subG. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)