Convex independence forbids collinear triples

import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Foundation
import Mathlib.Analysis.Convex.Between
import Mathlib.Analysis.Convex.Independent
import Mathlib.Data.Finset.Basic
import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
open Problem97 Problem97.ConvexIndep
open scoped EuclideanGeometry

theorem Batch3N9.Problem97.ConvexIndep.not_three_collinear {A : Finset ℝ²} (hA : ConvexIndep A) {x y z : ℝ²} (hx : x ∈ A) (hy : y ∈ A) (hz : z ∈ A) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) (hcol : Collinear ℝ ({x, y, z} : Set ℝ²)) : False := by sorry