proposition: Lemma atrans_dvd G S : [transitive G, on S | to] -> #|S| %| #|G|.
proof: Proof. by case/imsetP=> x _ ->; apply: dvdn_orbit. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)