proposition: Lemma eq_in_pcore pi rho G : {in \pi(G), pi =i rho} -> 'O_pi(G) = 'O_rho(G).
proof: Proof. move=> eq_pi_rho; apply/eqP; rewrite eqEsubset. by rewrite !sub_in_pcore // => p /eq_pi_rho->. 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)