proposition: Lemma gpath_connect t1 t2 : connect r t1 t2 -> {p | gpath t1 t2 p}.
proof: Proof. move=> t1Ct2. case: (pickP [pred p | gpath t1 t2 (p : `d[t1, t2].-tuple T)]) => [p Hp|HC]. by exists p. move: (t1Ct2); rewrite gdist_connect => dLT. absurd False => //. move: (dLT); rewrite -[#|_|](size_iota 0) -has_find. move => /(nth_find 0). rewrite -[find _ _]/`d[t1, t2]. rewrite nth_iota // add0n => /connectnP[p [H1p H2p /eqP H3p]]. have /idP[] := HC (Tuple H3p). by apply/and3P; split=> //=; apply/eqP=> //; rewrite (eqP H3p). Qed.
imports: mathcomp(all_ssreflect)