proposition: Lemma semiregular_prime H K : semiregular K H -> semiprime K H.
proof: Proof. move=> regH x Hx; apply/eqP; rewrite eqEsubset {1}regH // sub1G. by rewrite -cent_set1 setIS ?centS // sub1set; case/setD1P: Hx. 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)