proposition: Lemma acts_dom A S : [acts A, on S | to] -> A \subset D.
proof: Proof. by move=> nSA; rewrite (subset_trans nSA) ?subsetIl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)