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.

1∀ (n : ℕ),2  3 ≤ n →3    ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)),4      Function.Injective p →5        EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2