proposition: Lemma pseries_sub_catl pi1s pi2s gT (G : {group gT}) : pseries pi1s G \subset pseries (pi1s ++ pi2s) G.
proof: Proof. elim/last_ind: pi2s => [|pi pis IHpi]; rewrite ?cats0 // -rcons_cat. by rewrite pseries_rcons; apply: subset_trans IHpi _; rewrite sub_cosetpre. 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)