have := h'.dist
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
⊢ False
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w u v x : V
h : sbtw u v x
h' : sbtw v u x
this : Dist.dist v u + Dist.dist u x = Dist.dist v x
⊢ False