proposition: Lemma tnth_ord_tuple i : tnth ord_tuple i = i.
proof: Proof. apply: val_inj; rewrite (tnth_nth i) -(nth_map _ 0) ?size_tuple //. by rewrite /= enumT unlock val_ord_enum nth_iota. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)