proposition: Lemma pcore_mod_res pi gT rT (D : {group gT}) (f : {morphism D >-> rT}) : f @* pcore_mod D pi (F _ D) \subset pcore_mod (f @* D) pi (F _ (f @* D)).
proof: Proof. exact: morphim_pcore_mod. 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)