proposition: Lemma dtuple_on_subset n (S1 S2 : {set sT}) t : S1 \subset S2 -> t \in n.-dtuple(S1) -> t \in n.-dtuple(S2).
proof: Proof. by move=> sS12 /[!inE] /andP[-> /subset_trans]; apply. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)