proposition: Lemma pseries_sub_catr pi1s pi2s gT (G : {group gT}) : pseries pi2s G \subset pseries (pi1s ++ pi2s) G.
proof: Proof. elim: pi1s => //= pi1 pi1s /subset_trans; apply. elim/last_ind: {pi1s pi2s}(_ ++ _) => [|pis pi IHpi]; first exact: sub1G. rewrite -rcons_cons (pseries_rcons _ (pi1 :: pis)). rewrite -sub_morphim_pre ?pseries_norm2 //. apply: pcore_max; last by rewrite morphim_normal ?pseries_normal. have: pi.-group (pseries (rcons pis pi) G / pseries pis G). by rewrite quotient_pseries pcore_pgroup. by apply: pnat_dvd; rewrite !card_quotient ?pseries_norm2 // indexgS. 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)