proposition: Lemma atrans_acts_card G S : [transitive G, on S | to] = [acts G, on S | to] && (#|orbit to G @: S| == 1%N).
proof: Proof. apply/idP/andP=> [GtrS | [nSG]]. split; first exact: atrans_acts. rewrite ((_ @: S =P [set S]) _) ?cards1 // eqEsubset sub1set. apply/andP; split=> //; apply/subsetP=> _ /imsetP[x Sx ->]. by rewrite inE (atransP GtrS). rewrite eqn_leq andbC lt0n => /andP[/existsP[X /imsetP[x Sx X_Gx]]]. rewrite (cardD1 X) {X}X_Gx imset_f // ltnS leqn0 => /eqP GtrS. apply/imsetP; exists x => //; apply/eqP. rewrite eqEsubset acts_sub_orbit // Sx andbT. apply/subsetP=> y Sy; have:= card0_eq GtrS (orbit to G y). by rewrite !inE /= imset_f // andbT => /eqP <-; apply: orbit_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)