have hbcd : sbtw b c d := by
  refine sbtw_mk habc.2.1.ne hacd.ne23 ?_
  rw [Delta] at this
  linarith [hacd.dist]
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
⊢ False
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
habc : SimpleTriangle a b c
hacd : sbtw a c d
this : dist a d + Delta a b c ≤ dist a b + dist b d
hbcd : sbtw b c d
⊢ False