proposition: Lemma card_uniq_tuple n (t : n.-tuple sT) : uniq t -> #|t| = n.
proof: Proof. by move/card_uniqP->; apply: size_tuple. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)