proposition: Lemma Frobenius_index_dvd_ker1 : #|G : K| %| #|K|.-1.
proof: Proof. have[defG _ _ /andP[sKG _] _] := Frobenius_context. by rewrite -divgS // -(sdprod_card defG) mulKn ?Frobenius_dvd_ker1. 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)