proposition: Lemma Frobenius_ker_Hall : Hall G K.
proof: Proof. have [_ _ _ /andP[sKG _] _] := Frobenius_context. by rewrite /Hall sKG Frobenius_index_coprime. 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)