proposition: Lemma semiprimeJ K H x : semiprime K H -> semiprime (K :^ x) (H :^ x).
proof: Proof. move=> prH yx; rewrite -conjD1g => /imsetP[y Hy ->]. by rewrite cent1J centJ -!conjIg prH. 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)