proposition: Lemma tuto_tnth_nth : forall (x : T) (t : n.-tuple T) i, tnth t i = nth x t i.
proof: Proof. by move=> x t i; apply: set_nth_default; rewrite size_tuple. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)