have habd : sbtw a b d := by
  refine sbtw_mk habc.1.ne h.ne ?_
  have := habc_min _ _ _ hbcd
  rw [Delta, 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
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c 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
habc_min : ∀ (a' b' c' : V), SimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c'
hacd : sbtw a c d
hcd : SimpleEdges.Adj c d
h : SimpleEdges.Adj b d
hbcd : SimpleTriangle b c d
habd : sbtw a b d
⊢ False