proposition: Lemma gpath_catr t1 t2 p1 p2 : gpath t1 t2 (p1 ++ p2) -> gpath (last t1 p1) t2 p2.
proof: Proof. move=> /gpathP[]. rewrite cat_path last_cat => /andP[t1Pp1 t1p1LPp2] t1p1Lp2Lt2 dt1t2E. apply/gpathP; split => //. have : `d[last t1 p1, t2] <= size p2 by rewrite gdist_path_le. rewrite leq_eqVlt => /orP[/eqP//|dLSp1]. have /gpath_connect[p3 /gpathP[H1 H2 H3]] : connect r (last t1 p1) t2 by apply/connectP; exists p2. have : size (p1 ++ p3) < `d[t1, t2] by rewrite dt1t2E !size_cat -H3 ltn_add2l. rewrite ltnNge => /negP[]. apply: gdist_path_le; first by rewrite cat_path H1 andbT. by rewrite last_cat. Qed.
imports: mathcomp(all_ssreflect)