proposition: Lemma tnth_nseq x i : tnth [tuple of nseq n x] i = x.
proof: Proof. by rewrite !(tnth_nth (tnth_default (nseq_tuple x) i)) nth_nseq ltn_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)