proposition: Lemma porbit_set_astabs s X : X \in porbit_set s -> s \in 'N(X | 'P).
proof: Proof. Proof using. rewrite /astabs !inE /= => /andP[/imsetP[x0 _ -> {X} _]]. apply/subsetP => x; rewrite inE apermE. rewrite -!eq_porbit_mem => /eqP <-. by rewrite -{2}(expg1 s) porbit_perm. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp