proposition: Lemma gdist_sym t1 t2 : `d[t1, t2]_r = `d[t2, t1]_(fun z : T => r^~ z).
proof: Proof. apply: eq_find => i. apply/connectnP/connectnP => /= [] [p [H1p H2p H3p]]. exists (rev (belast t1 p)); split => //. - by rewrite -H2p rev_path. - rewrite -H2p; case: (p) => //= a p1. by rewrite rev_cons last_rcons. by rewrite size_rev size_belast. exists (rev (belast t2 p)); split => //. - by rewrite -H2p rev_path. - rewrite -H2p; case: (p) => //= a p1. by rewrite rev_cons last_rcons. by rewrite size_rev size_belast. Qed.
imports: mathcomp(all_ssreflect)