proposition: Lemma semiprime_regular H K : semiprime K H -> 'C_K(H) = 1 -> semiregular K H.
proof: Proof. by move=> prKH tiKcH x Hx; rewrite prKH. 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)