proposition: Lemma morphim_pcore pi : GFunctor.pcontinuous (@pcore pi).
proof: Proof. move=> gT rT D G f; apply/bigcapsP=> M /normal_sub_max_pgroup; apply. by rewrite morphim_pgroup ?pcore_pgroup. by apply: morphim_normal; apply: 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)