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