proposition: Theorem stab_ntransitiveI m x : x \in S -> [transitive G, on S | to] -> [transitive^m 'C_G[x | to], on S :\ x | to] -> [transitive^m.+1 G, on S | to].
proof: Proof. move=> Sx Gtr Gntr. have t_to_x t: t \in m.+1.-dtuple(S) -> exists2 a, a \in G & exists2 t', t' \in m.-dtuple(S :\ x) & t = n_act to [tuple of x :: t'] a. - case/tupleP: t => y t St. have Sy: y \in S by rewrite dtuple_on_add_D1 in St; case/andP: St. rewrite -(atransP Gtr _ Sy) in Sx; case/imsetP: Sx => a Ga toya. exists a^-1; first exact: groupVr. exists (n_act to t a); last by rewrite n_act_add toya !actK. move/(n_act_dtuple (subsetP (atrans_acts Gtr) a Ga)): St. by rewrite n_act_add -toya dtuple_on_add_D1 => /andP[]. case: (imsetP Gntr) => t dt S_tG; pose xt := [tuple of x :: t]. have dxt: xt \in m.+1.-dtuple(S) by rewrite dtuple_on_add_D1 Sx. apply/imsetP; exists xt => //; apply/setP=> t2. apply/esym; apply/imsetP/idP=> [[a Ga ->] | ]. by apply: n_act_dtuple; rewrite // (subsetP (atrans_acts Gtr)). case/t_to_x=> a2 Ga2 [t2']; rewrite S_tG. case/imsetP=> a /setIP[Ga /astab1P toxa] -> -> {t2 t2'}. by exists (a * a2); rewrite (groupM, actM) //= !n_act_add toxa. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)