proposition: Lemma Frobenius_coprime : coprime #|K| #|H|.
proof: Proof. by rewrite (coprime_dvdr Frobenius_dvd_ker1) ?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)