fact: Definition valid_edge : edge -> Plane R -> bool := fun g p => (left_pt g).1 <= p.1 <= (right_pt g).1.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection