proposition: Theorem stab_ntransitive m x : 0 < m -> x \in S -> [transitive^m.+1 G, on S | to] -> [transitive^m 'C_G[x | to], on S :\ x | to].
proof: Proof. move=> m_gt0 Sx Gtr; have sSxS: S :\ x \subset S by rewrite subsetDl. case: (imsetP Gtr); case/tupleP=> x1 t1; rewrite dtuple_on_add. case/and3P=> Sx1 nt1x1 dt1 trt1; have Gtr1 := ntransitive1 (ltn0Sn _) Gtr. case: (atransP2 Gtr1 Sx1 Sx) => // a Ga x1ax. pose t := n_act to t1 a. have dxt: [tuple of x :: t] \in m.+1.-dtuple(S). by rewrite trt1 x1ax; apply/imsetP; exists a => //; apply: val_inj. apply/imsetP; exists t; first by rewrite dtuple_on_add_D1 Sx in dxt. apply/setP=> t2; apply/idP/imsetP => [dt2|[b]]. have: [tuple of x :: t2] \in dtuple_on _ S by rewrite dtuple_on_add_D1 Sx. case/(atransP2 Gtr dxt)=> b Gb [xbx tbt2]. by exists b; [rewrite inE Gb; apply/astab1P | apply: val_inj]. case/setIP=> Gb /astab1P xbx ->{t2}. rewrite n_act_dtuple //; last by rewrite dtuple_on_add_D1 Sx in dxt. apply/astabsP=> y; rewrite !inE -{1}xbx (inj_eq (act_inj _ _)). by rewrite (actsP (atrans_acts Gtr1)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)