proposition: Lemma pseries_catr_id pi1s pi2s gT (G : {group gT}) : pseries pi2s (pseries (pi1s ++ pi2s) G) = pseries pi2s G.
proof: Proof. elim/last_ind: pi2s => [//|pi2s pi IHpi] in G *. have Epis: pseries pi2s (pseries (pi1s ++ rcons pi2s pi) G) = pseries pi2s G. by rewrite -cats1 catA -2!IHpi pseries_catl_id. apply: (@quotient_inj _ (pseries_group pi2s G)). - by rewrite /= -Epis /(_ <| _) pseries_norm2 -cats1 pseries_sub_catl. - by rewrite /= /(_ <| _) pseries_norm2 -cats1 pseries_sub_catl. rewrite /= -Epis {1}quotient_pseries Epis quotient_pseries. apply/eqP; rewrite eqEsubset !pcore_max ?pcore_pgroup //=. rewrite -quotient_pseries morphim_normal // /(_ <| _) pseries_norm2. by rewrite pseries_sub_catr. by rewrite gFnormal_trans ?morphim_normal ?gFnormal. 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)