proposition: Lemma pseries_group_set : group_set pseries.
proof: Proof. by rewrite /pseries; case: rev => [|pi1 pi1']; apply: groupP. 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)