proposition: Lemma atrans_supgroup G H S : G \subset H -> [transitive G, on S | to] -> [transitive H, on S | to] = [acts H, on S | to].
proof: Proof. move=> sGH trG; apply/idP/idP=> [|actH]; first exact: atrans_acts. case/imsetP: trG => x Sx defS; apply/imsetP; exists x => //. by apply/eqP; rewrite eqEsubset acts_sub_orbit ?Sx // defS imsetS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)