proposition: Lemma pcoreJ G x : 'O_pi(G :^ x) = 'O_pi(G) :^ x.
proof: Proof. apply/eqP; rewrite eqEsubset -sub_conjgV. rewrite !pcore_max ?pgroupJ ?pcore_pgroup ?normalJ ?pcore_normal //. by rewrite -(normalJ _ _ x) conjsgKV pcore_normal. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)