simp only [dist_le_zero] at h
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : dist v u ≤ 0
⊢ False
V : Type u_1
inst✝ : MetricSpace V
u v : V
h12 : u ≠ v
h23 : v ≠ u
h : v = u
⊢ False