proposition: Lemma regular_norm_coprime K H : H \subset 'N(K) -> semiregular K H -> coprime #|K| #|H|.
proof: Proof. move=> nKH regH. by rewrite (coprime_dvdr (regular_norm_dvd_pred nKH regH)) ?coprimenP. 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)