proposition: Lemma cent_semiregular H K X : semiregular K H -> X \subset H -> X :!=: 1 -> 'C_K(X) = 1.
proof: Proof. move=> regKH sXH /trivgPn[x Xx ntx]; apply/trivgP. rewrite -(regKH x) ?inE ?(subsetP sXH) ?ntx ?setIS //=. by rewrite -cent_cycle 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)