proposition: Lemma gdist_path_le t1 t2 p : path r t1 p -> last t1 p = t2 -> `d[t1, t2] <= size p.
proof: Proof. move=> Hp Hl. have [tLp|pLt] := leqP #|T| (size p). apply: leq_trans tLp. by apply: gdist_card_le. have F : t2 \in connectn (size p) t1. by apply/connectnP; exists p. case: leqP => // /(before_find _) // /(_ 0). by rewrite seq.nth_iota // F. Qed.
imports: mathcomp(all_ssreflect)