proposition: Lemma quotient_pseries_cat pi1s pi2s gT (G : {group gT}) : pseries (pi1s ++ pi2s) G / pseries pi1s G = pseries pi2s (G / pseries pi1s G).
proof: Proof. elim/last_ind: pi2s => [|pi2s pi IHpi]; first by rewrite cats0 trivg_quotient. have psN := pseries_normal _ G; set K := pseries _ G. case: (third_isom (pseries_sub_catl pi1s pi2s G) (psN _)) => //= f inj_f im_f. have nH2H: pseries pi2s (G / K) <| pseries (pi1s ++ rcons pi2s pi) G / K. rewrite -IHpi morphim_normal // -cats1 catA. by apply/andP; rewrite pseries_sub_catl pseries_norm2. apply: (quotient_inj nH2H). by apply/andP; rewrite /= -cats1 pseries_sub_catl pseries_norm2. rewrite /= quotient_pseries /= -IHpi -rcons_cat. rewrite -[G / _ / _](morphim_invm inj_f) //= {2}im_f //. rewrite -(@injmF [igFun of @pcore pi]) /= ?injm_invm ?im_f // -quotient_pseries. by rewrite -im_f ?morphim_invm ?morphimS ?normal_sub. 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)