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