proposition: Lemma subgroup_transitivePin G H S x : x \in S -> H \subset G -> G \subset D -> [transitive G, on S | to] -> reflect ('C_G[x | to] * H = G) [transitive H, on S | to].
proof: Proof. move=> Sx sHG sGD trG; have sHD := subset_trans sHG sGD. apply: (iffP idP) => [trH | defG]. rewrite group_modr //; apply/setIidPl/subsetP=> a Ga. have Sxa: to x a \in S by rewrite (acts_act (atrans_acts_in sGD trG)). have [b Hb xab]:= atransP2in sHD trH Sxa Sx. have Da := subsetP sGD a Ga; have Db := subsetP sHD b Hb. rewrite -(mulgK b a) mem_mulg ?groupV // !inE groupM //= sub1set inE. by rewrite actMin -?xab. apply/imsetP; exists x => //; apply/setP=> y; rewrite -(atransPin sGD trG Sx). apply/imsetP/imsetP=> [] [a]; last by exists a; first apply: (subsetP sHG). rewrite -defG => /imset2P[c b /setIP[_ cxc] Hb ->] ->. exists b; rewrite ?actMin ?(astab_dom cxc) ?(subsetP sHD) //. by rewrite (astab_act cxc) ?inE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)