proposition: Lemma dtuple_on_add_D1 n x (t : n.-tuple sT) : ([tuple of x :: t] \in n.+1.-dtuple(S)) = (x \in S) && (t \in n.-dtuple(S :\ x)).
proof: Proof. rewrite dtuple_on_add !inE (andbCA (~~ _)); do 2!congr (_ && _). rewrite -!(eq_subset (in_set [in t])) setDE setIC subsetI; congr (_ && _). by rewrite -setCS setCK sub1set !inE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)