proposition: Lemma pseries_char_catr pi1s pi2s gT (G : {group gT}) : pseries pi2s G \char pseries (pi1s ++ pi2s) G.
proof: Proof. by rewrite -(pseries_catr_id pi1s pi2s G) pseries_char. 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)