Lean: 'not in convex position' proofs via a vertical segment between two chords

To show a planar point b is NOT a vertex of a convex polygon (Mathlib ConvexIndependent, via convexIndependent_set_iff_notMem_convexHull_sdiff), skip Carathéodory and triangle case splits. Use one lemma: if a.1 < b.1 < c.1, d.1 < b.1 < e.1, slope a c ≤ slope a b (b above chord ac) and slope d b ≤ slope d e (b below chord de), then b ∈ convexHull {a,c,d,e}. Proof: u = a + t•(c-a) and w = d + s•(e-d) with t,s chosen so that u.1 = w.1 = b.1 (Convex.add_smul_sub_mem twice). Then b = u + l•(w-u) with l = (b.2-u.2)/(w.2-u.2). If w.2 = u.2, div_zero makes l = 0 and still works. Every 4-point convexity violation in the Erdős–Szekeres 1961 lower-bound construction (2^(n-2) points, no convex n-gon) is an instance, including 'a convex polygon with distinct x splits into a lower cup and an upper cap' (split by the chord from leftmost to rightmost point).