proposition: Lemma semiregularJ K H x : semiregular K H -> semiregular (K :^ x) (H :^ x).
proof: Proof. move=> regH yx; rewrite -conjD1g => /imsetP[y Hy ->]. by rewrite cent1J -conjIg regH ?conjs1g. 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)