Theorem: SBtw.sbtw.right_cancel (LeanCamCombi/MetricBetween.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u✝ v✝ w✝ u v w x : V
h : sbtw u v x
h' : sbtw v w x
⊢ Dist.dist u v + Dist.dist v w ≤ Dist.dist u w
Tactic:
linarith [h.dist, h'.dist, dist_triangle u w x, dist_triangle u v w]
State after:
no goals