proposition: Lemma astabs_actby S : 'N(S | <[nRA]>) = 'N_A(R :&: S | to).
proof: Proof. apply/setP=> a; rewrite setIA (setIidPl (acts_dom nRA)) !inE. case Aa: (a \in A) => //=; apply/subsetP/subsetP=> nRSa x => [|Sx]. by case/setIP=> Rx /nRSa; rewrite !inE actbyE ?(acts_act nRA) ?Rx. have:= nRSa x; rewrite !inE /= /actby Aa Sx ?(acts_act nRA) //. by case: (x \in R) => //; apply. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)