proposition: Lemma stab_porbit S s : s \in 'N(S | 'P) -> forall x, (x \in S) = (porbit s x \subset S).
proof: Proof. Proof using. move=> Hs x; apply/idP/subsetP => [Hx y /porbitP[i ->{y}] | Hsubs]. - elim: i => [|i]; first by rewrite expg0 perm1. by rewrite expgSr permM; move: Hs => /astabsP <- /=. - exact: Hsubs (porbit_id s x). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype