proposition: Lemma actsD : [acts A, on S :\: T | to].
proof: Proof. by apply: subset_trans astabsD; rewrite subsetI AactS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)