Theorem: sbtw_iff_of_ne (LeanCamCombi/MetricBetween.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
h12 : u ≠ v
h13 : u ≠ w
h23 : v ≠ w
⊢ sbtw u v w ↔ dist u v + dist v w = dist u w
Tactic:
simp [MetricSpace.sbtw_iff, h12, h13, h23]
State after:
no goals