If $n$ distinct points in ${\mathbb{R}}^2$ form a convex polygon then some vertex has at least $\lfloor \frac{n}{2}\rfloor$ different distances to other vertices.

AMS 52 · open (literature)

theorem erdos_982 (n : ℕ) (hn : 3 ≤ n) (p : Fin n → ℝ²) (hp : Function.Injective p)
    (hp' : EuclideanGeometry.IsConvexPolygon p) :
    ∃ (i : Fin n), { d : ℝ | ∃ j : Fin n, j ≠ i ∧ d = dist (p i) (p j) }.ncard ≥ n / 2