proposition: Lemma gdist_succ t1 t2 : 0 < `d[t1, t2] < #|T| -> {t3 | r t1 t3 /\ `d[t3, t2] = `d[t1, t2].-1}.
proof: Proof. case/andP => dP dT. move: dT dP. rewrite -gdist_connect => /gpath_connect[[|t3 p] pH]. by rewrite (gpath_dist pH). exists t3; split. by have /andP[] := gpath_path (@gpath_catl _ _ [::t3] _ pH). by rewrite (gdist_cons pH). Qed.
imports: mathcomp(all_ssreflect)