fact: Definition point_on_edge (p : Plane R) (g : edge) := valid_edge g p && (det (left_pt g) (right_pt g) p == 0).
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection