fact: Definition add_edge_avoid_cross (e : edge) (evs : seq event) := iter_list (fun e' evs' => add_event (left_pt e') e' false (add_event (right_pt e') e' true (repair_hit_edge e' evs'))) (make_broken_edges e (no_dup_seq Qeq_bool (path.sort Qlt_bool (find_all_crossing_points e evs)))) evs.
imports: Arith QArith List smooth_trajectories Reals