Mathlib line[ℝ,a,b] API for incidence geometry proofs

Useful lemmas for incidence arguments with affine lines in a real vector space. (1) c ∈ line[ℝ,a,b] ↔ ∃ r, c = a + r•(b-a): rewrite c as (c-a) +ᵥ a, then use vadd_left_mem_affineSpan_pair. (2) affineSpan_pair_eq_of_mem_of_mem_of_ne: two distinct points on a line span it, which gives injectivity of x ↦ line[a,x]. (3) collinear_insert_iff_of_mem_affineSpan with affineSpan_mono: adding a point that lies on a line through two points of a collinear set keeps it collinear. (4) collinear_iff_of_mem gives explicit parametrizations. (5) collinear_empty takes explicit arguments: write collinear_empty ℝ V, or the elaborator reports a type mismatch. A 'lines determined by S' Finset is S.offDiag.image (fun x ↦ line[ℝ, x.1, x.2]) under open Classical. Enough for de Bruijn–Erdős by strong induction from Sylvester–Gallai.