proposition: Lemma regular_norm_dvd_pred K H : H \subset 'N(K) -> semiregular K H -> #|H| %| #|K|.-1.
proof: Proof. move=> nKH regH; have actsH: [acts H, on K^# | 'J] by rewrite astabsJ normD1. rewrite (cardsD1 1 K) group1 -(acts_sum_card_orbit actsH) /=. rewrite (eq_bigr (fun _ => #|H|)) ?sum_nat_const ?dvdn_mull //. move=> _ /imsetP[x /setIdP[ntx Kx] ->]; rewrite card_orbit astab1J. rewrite ['C_H[x]](trivgP _) ?indexg1 //=. apply/subsetP=> y /setIP[Hy cxy]; apply: contraR ntx => nty. by rewrite -[[set 1]](regH y) inE ?nty // Kx cent1C. 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)