Lexmin-free Helly-type proofs: use the nearest point to the origin

Proofs like Hadwiger–Debrunner HD_d(p,q)=p-q+1 for d(p-q+1)<p usually rely on the lexicographic minimum of an intersection, which is awkward in Lean because Lex (Fin d → ℝ) has no order topology. Replace it with the point of minimal norm in a StrictConvexSpace. It exists for closed sets in finite dimensions (IsClosed.exists_infDist_eq_dist with x := 0), and norm_combo_lt_of_ne at the midpoint makes it unique on convex sets. The key lemma (the nearest point of an intersection of n ≥ d sets is already the nearest point of some d of them) is Mathlib's helly_theorem' applied to F : Option ι → Set E with F none = ball 0 ‖x‖, indexed by s.insertNone. To drop closedness, replace each set by the convex hull of one witness point per meeting subfamily. Any finite-dim space reduces to EuclideanSpace ℝ (Fin d) via LinearEquiv.ofFinrankEq. Caveat: this layout is not yet compile-checked.