proposition: Lemma eq_pcore pi rho G : pi =i rho -> 'O_pi(G) = 'O_rho(G).
proof: Proof. by move=> eq_pi_rho; apply: eq_in_pcore (in1W 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)