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