proposition: Lemma ntransitive_weak k m : k <= m -> [transitive^m G, on S | to] -> [transitive^k G, on S | to].
proof: Proof. move/subnKC <-; rewrite addnC; elim: {m}(m - k) => // m IHm. rewrite addSn => tr_m1; apply: IHm; move: {m k}(m + k) tr_m1 => m tr_m1. have ext_t t: t \in dtuple_on m S -> exists x, [tuple of x :: t] \in m.+1.-dtuple(S). - move=> dt. have [sSt | /subsetPn[x Sx ntx]] := boolP (S \subset t); last first. by exists x; rewrite dtuple_on_add andbA /= Sx ntx. case/imsetP: tr_m1 dt => t1 /[!inE] /andP[Ut1 St1] _ /andP[Ut _]. have /subset_leq_card := subset_trans St1 sSt. by rewrite !card_uniq_tuple // ltnn. case/imsetP: (tr_m1); case/tupleP=> [x t]; rewrite dtuple_on_add. case/and3P=> Sx ntx dt; set xt := [tuple of _] => tr_xt. apply/imsetP; exists t => //. apply/setP=> u; apply/idP/imsetP=> [du | [a Ga ->{u}]]. case: (ext_t u du) => y; rewrite tr_xt. by case/imsetP=> a Ga [_ def_u]; exists a => //; apply: val_inj. have: n_act to xt a \in dtuple_on _ S by rewrite tr_xt imset_f. by rewrite n_act_add dtuple_on_add; case/and3P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)