proposition: Lemma Frobenius_ker_dvd_ker1 G K : [Frobenius G with kernel K] -> #|G : K| %| #|K|.-1.
proof: Proof. by case/existsP=> H; apply: Frobenius_index_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)