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