fact: Definition Frobenius_group_with_kernel G K := [exists H : {group gT}, Frobenius_group_with_kernel_and_complement G K H].
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)