fact: Definition cell_safe_exits_left (c : cell) : seq vert_edge := let lx := (seq.head dummy_pt (left_pts c)).1 in map (fun p => Build_vert_edge lx (fst p).2 (snd p).2) (seq_to_intervals (left_pts c)).
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection