Erdős 982: add the solved concyclic variant and Lean proof

I plan to add a solved concyclic variant of Erdős problem 982 to the existing
`FormalConjectures/ErdosProblems/982.lean` file.

For distinct points on a common circle, every chosen vertex determines at
least `n / 2` distinct distances to the other points. This needs neither the
convex-polygon hypothesis nor `3 ≤ n`. A zero-`sorry` Lean 4 proof is
available and will be linked with `formal_proof using lean4`.

This will modify the existing file rather than introduce a duplicate problem
file. Related history: #1053 and the closed duplicate-file attempt #2981.

Disclosure: the Lean proof and analysis were AI-generated under human
direction; this exposition was human-prepared, and Lean’s kernel
machine-checked the proof.

Start in FormalConjectures/ErdosProblems/982.lean and review the existing Erdős 982 formalization and nearby conventions. Add the solved concyclic variant there, using the stated common-circle distance claim and the available zero-sorry Lean 4 proof. Done means the proof is accepted by Lean 4 and the formal_proof using lean4 link is included.

Written by the indexing model from the issue text.