proposition: Lemma gdist_triangular t1 t2 t3 : `d[t1, t2] <= `d[t1, t3] + `d[t3, t2].
proof: Proof. have [/gpath_connect[p pH]|/gdist_nconnect->] := boolP (connect r t1 t3); last first. by apply: leq_trans (gdist_card_le _ _) (leq_addr _ _). have [/gpath_connect [p2 p2H] |/gdist_nconnect->] := boolP (connect r t3 t2); last first. by apply: leq_trans (gdist_card_le _ _) (leq_addl _ _). rewrite (gpath_dist pH) (gpath_dist p2H) -size_cat. apply: gdist_path_le. rewrite cat_path (gpath_path pH). by rewrite (gpath_last pH) (gpath_path p2H). by rewrite last_cat (gpath_last pH) (gpath_last p2H). Qed.
imports: mathcomp(all_ssreflect)