proposition: Lemma pseries_rcons_id pis pi gT (G : {group gT}) : pseries (rcons (rcons pis pi) pi) G = pseries (rcons pis pi) G.
proof: Proof. apply/eqP; rewrite -!cats1 eqEsubset pseries_sub_catl andbT -catA. rewrite -(quotientSGK _ (pseries_sub_catl _ _ _)) ?pseries_norm2 //. rewrite !quotient_pseries_cat -quotient_sub1 ?pseries_norm2 //. by rewrite quotient_pseries_cat /= !pseries1 trivg_pcore_quotient. 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)