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