proposition: Lemma Frobenius_dvd_ker1 : #|H| %| #|K|.-1.
proof: Proof. apply: regular_norm_dvd_pred Frobenius_reg_ker. by have[/sdprodP[]] := Frobenius_context. 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)