proposition: Lemma coprime_pcoreC (rT : finGroupType) pi G (R : {group rT}) : coprime #|'O_pi(G)| #|'O_pi^'(R)|.
proof: Proof. exact: pnat_coprime (pcore_pgroup _ _) (pcore_pgroup _ _). 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)