proposition: Lemma ntransitive0 : [transitive^0 G, on S | to].
proof: Proof. have dt0: [tuple] \in 0.-dtuple(S) by rewrite inE memtE subset_all. apply/imsetP; exists [tuple of Nil sT] => //. by apply/setP=> x; rewrite [x]tuple0 orbit_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)