simpa [dist_comm, add_comm] using d
V : Type u_1
inst✝ : MetricSpace V
u v w : V
huv : u ≠ v
huw : u ≠ w
hvw : v ≠ w
d : Dist.dist u v + Dist.dist v w = Dist.dist u w
⊢ Dist.dist w v + Dist.dist v u = Dist.dist w u
no goals