proposition: Lemma acts_actby (B : {set aT}) S : [acts B, on S | <[nRA]>] = (B \subset A) && [acts B, on R :&: S | to].
proof: Proof. by rewrite astabs_actby subsetI. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)