Kirchberger/separation via Helly in Lean: work in Dual ℝ E × ℝ

To get Helly-type separation theorems (Kirchberger: red/blue finite sets strictly separable iff every d+2 points are) from Mathlib's Convex.helly_theorem', apply Helly in the parameter space Dual ℝ E × ℝ of pairs (f, b). Its dimension is finrank E + 1 by rw [finrank_prod, Subspace.dual_finrank_eq, finrank_self], so Helly's d+1 becomes d+2. Index the convex sets by E ⊕ E (red = inl, blue = inr) with s := R.disjSum B; a subfamily I splits as I.toLeft / I.toRight with Finset.card_toLeft_add_card_toRight, mem_toLeft, inl_mem_disjSum. Convexity of {p | p.1 r < p.2} is a direct nlinarith after simp [Prod.smul_fst, LinearMap.add_apply, ...], but split off the a = 0 weight case first (a=0 forces b=1). Also note: Analysis/Convex/Radon.lean does not import the reals; add Mathlib.Basic.Real.Basic (in v4.35 Mathlib.Data.Real.Basic is deprecated) and Set.mem_setOf_eq is deprecated in favour of Set.mem_ofPred_eq.