proposition: Lemma ntransitive1 m : 0 < m -> [transitive^m G, on S | to] -> [transitive G, on S | to].
proof: Proof. have trdom1 x: ([tuple x] \in 1.-dtuple(S)) = (x \in S). by rewrite dtuple_on_add !inE memtE subset_all andbT. move=> m_gt0 /(ntransitive_weak m_gt0) {m m_gt0}. case/imsetP; case/tupleP=> x t0; rewrite {t0}(tuple0 t0) trdom1 => Sx trx. apply/imsetP; exists x => //; apply/setP=> y; rewrite -trdom1 trx. by apply/imsetP/imsetP=> [[a ? [->]]|[a ? ->]]; exists a => //; apply: val_inj. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)