proposition: Lemma semiregular1l H : semiregular 1 H.
proof: Proof. by move=> x _ /=; rewrite setI1g. 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)