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