fact: Definition Frobenius_action := [/\ [faithful G, on S | to], [transitive G, on S | to], {in G^#, forall x, #|'Fix_(S | to)[x]| <= 1}, H != 1 & exists2 u, u \in S & H = 'C_G[u | to]].
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)