proposition: Lemma semiprimeS K1 K2 A1 A2 : K1 \subset K2 -> A1 \subset A2 -> semiprime K2 A2 -> semiprime K1 A1.
proof: Proof. move=> sK12 sA12 prKA2 x /setD1P[ntx A1x]. apply/eqP; rewrite eqEsubset andbC -{1}cent_set1 setIS ?centS ?sub1set //=. rewrite -(setIidPl sK12) -!setIA prKA2 ?setIS ?centS //. by rewrite !inE ntx (subsetP sA12). 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)