proposition: Lemma stab_semiprime H K X : semiprime K H -> X \subset K -> 'C_H(X) != 1 -> 'C_H(X) = H.
proof: Proof. move=> prKH sXK ntCHX; apply/setIidPl; rewrite centsC -subsetIidl. rewrite -{2}(setIidPl sXK) -setIA -(cent_semiprime prKH _ ntCHX) ?subsetIl //. by rewrite !subsetI subxx sXK centsC subsetIr. 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)