exact hc'.ne12 this
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 c b ≤ dist c' b
this : c = c'
⊢ False
no goals