proposition: Lemma pseries_subfun pis : GFunctor.closed (@pseries pis) /\ GFunctor.pcontinuous (@pseries pis).
proof: Proof. elim/last_ind: pis => [|pis pi [sFpi fFpi]]. by split=> [gT G | gT rT D G f]; rewrite (sub1G, morphim1). pose fF := [gFun by fFpi : GFunctor.continuous [igFun by sFpi & fFpi]]. pose F := [pgFun by fFpi : GFunctor.hereditary fF]. split=> [gT G | gT rT D G f]; rewrite !pseries_rcons ?(pcore_mod_sub F) //. exact: (morphim_pcore_mod F). 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)