Small planar order-type facts in Lean: turn signs + transitivity rules + decide

To prove Klein's theorem (5 points, no 3 collinear ⇒ 4 in convex position) without convex-hull case analysis: sort by x (shear first; sort via Finset.orderEmbOfFin on the image of Prod.fst, then choose a point per x), define turn a b c := decide (slope a b < slope b c). For sorted a<b<c<d the three-slope lemma gives four Bool rules on t1=abc,t2=abd,t3=acd,t4=bcd (one per point: e.g. at a, t1=t3 → t2=t1), proved by rcases on four turn_cases (16 branches, first | decide | (exfalso; linarith)). Convexity criterion: all turns equal (cup/cap) or t2≠t3 (b,c on opposite sides of ad; separate each point with a linear functional). Then the combinatorial core over 10 Bool variables is closed by plain decide (1024 cases, fast, standard axioms). Gotcha: the cap case needs strict slope inequalities, so pass them in from turn_cases rather than decoding turn = false (which only gives ≤).