proposition: Lemma semiregularS K1 K2 A1 A2 : K1 \subset K2 -> A1 \subset A2 -> semiregular K2 A2 -> semiregular K1 A1.
proof: Proof. move=> sK12 sA12 regKA2 x /setD1P[ntx /(subsetP sA12)A2x]. by apply/trivgP; rewrite -(regKA2 x) ?inE ?ntx ?setSI. 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)