More than $(1/3+1/130)\,n$ distinct distances in general position for $n\ge 10000$

Let $n\ge 10000$ and let $p=(p_1,\dots,p_n)$ be an injective configuration of $n$ points in the plane, with image $P=\{p_1,\dots,p_n\}$. Assume that $P$ is in general position: no three points of $P$ are collinear and no four points of $P$ lie on a common circle. Let $D(P)$ be the number of distinct distances $|x-y|$ with $x,y\in P$ and $x\ne y$. Then

A circle about a point of $P$ contains at most three other points of $P$, which gives $3D(P)\ge n-1$. The theorem raises the coefficient $1/3$ by the explicit amount $1/130$ for every $n\ge 10000$. Erdős Problem 98 asks whether the minimum of $D(P)$ over general-position sets of $n$ points grows faster than every linear function of $n$; this theorem gives the linear lower bounds with coefficient at most $1/3+1/130$ only.

Formalization Note $D(P)$ is NumDistances p, the number of distances between distinct points of Config.toFinset p. General position is InGeneralPosition, in which "on a common circle" is Mathlib's Cospherical in the Euclidean plane.