fact: Record edge := Bedge { left_pt : Plane R; right_pt : Plane R; edge_cond : left_pt.1 < right_pt.1}.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection