proposition: Lemma dtuple_on_add n x (t : n.-tuple sT) : ([tuple of x :: t] \in n.+1.-dtuple(S)) = [&& x \in S, x \notin t & t \in n.-dtuple(S)].
proof: Proof. by rewrite !inE memtE !subset_all -!andbA; do !bool_congr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)