proposition: Lemma FrobeniusJgroup x G : [Frobenius G :^ x] = [Frobenius G].
proof: Proof. apply/existsP/existsP=> [] [H]. by rewrite -(conjsgKV x H) FrobeniusJcompl; exists (H :^ x^-1)%G. by exists (H :^ x)%G; rewrite FrobeniusJcompl. 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)