proposition: Lemma dtuple_onP t : reflect (injective (tnth t) /\ forall i, tnth t i \in S) (t \in dtuple_on).
proof: Proof. rewrite inE subset_all -forallb_tnth -[in uniq t]map_tnth_enum /=. by apply: (iffP andP) => -[/injectiveP-f_inj /forallP]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)