proposition: Lemma gdist_cat t1 t2 p1 p2 : gpath t1 t2 (p1 ++ p2) -> `d[t1,t2] = `d[t1, last t1 p1] + `d[last t1 p1, t2].
proof: Proof. move=> gH. rewrite (gpath_dist gH). rewrite (gpath_dist (gpath_catl gH)) (gpath_dist (gpath_catr gH)) //. by rewrite size_cat. Qed.
imports: mathcomp(all_ssreflect)