proposition: Lemma n_act_dtuple t a : a \in 'N(S | to) -> t \in dtuple_on -> n_act to t a \in dtuple_on.
proof: Proof. move/astabsP=> toSa /dtuple_onP[t_inj St]; apply/dtuple_onP. split=> [i j | i]; rewrite !tnth_map ?[_ \in S]toSa //. by move/act_inj; apply: t_inj. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)