have : dist b c ≤ dist b c' :=
  le_of_not_lt fun h => h.ne' <| hcmin _ (hc.trans_right' hc') h.le
case intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
⊢ False
case intro.intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b : V
hab : a ≠ b
c'✝ : V
hc'✝ : sbtw a c'✝ b
S : Set V := {x | sbtw a x b}
c : V
hc : sbtw a c b
hcmin : ∀ a' ∈ S, dist b a' ≤ dist b c → dist b c = dist b a'
c' : V
hc' : sbtw c c' b
this : dist b c ≤ dist b c'
⊢ False