fact: Definition UPath_tuple (up : UPath) : {n : 'I_#|G| & n.-tuple G} := let (p, Up) := up in existT _ (Ordinal (upath_size Up)) (in_tuple p).
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)