proposition: Lemma atrans_dvd_in G S : G \subset D -> [transitive G, on S | to] -> #|S| %| #|G|.
proof: Proof. move=> sGD transG; apply: dvdn_trans (atrans_dvd_index_in sGD transG) _. exact: dvdn_indexg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)