proposition: Lemma atrans_dvd_index_in G S : G \subset D -> [transitive G, on S | to] -> #|S| %| #|G : 'C_G(S | to)|.
proof: Proof. move=> sGD /imsetP[x Sx {1}->]; rewrite card_orbit_in //. by rewrite indexgS // setIS // astabS // sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)