fact: Definition point_strictly_under_edge (p : Plane R) (e : edge) : bool := det p (left_pt e) (right_pt e) < 0.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection