proposition: Lemma atrans_acts_in G S : G \subset D -> [transitive G, on S | to] -> [acts G, on S | to].
proof: Proof. move=> sGD transG; apply/subsetP=> a Ga; rewrite !inE (subsetP sGD) //. by apply/subsetP=> x /(atransPin sGD transG) <-; rewrite inE imset_f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)