Theorem: SBtw.sbtw.trans_right' (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
⊢ u ≠ w
Tactic:
rintro rfl
State after:
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

State before:
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
Tactic:
exact h.asymm_right h'
State after:
no goals

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
this : u ≠ w
⊢ Dist.dist u w + Dist.dist w x ≤ Dist.dist u x
Tactic:
linarith [h.dist, h'.dist, dist_triangle u v w]
State after:
no goals