fact: Definition break_edges_at_crossing (e1 e2 : edge) : option (edge * edge) * option (edge * edge) := let intersection_x := Qred (cross_first_coordinate e1 e2) in let new1 := if Qlt_bool (p_x (left_pt e1)) intersection_x && Qlt_bool intersection_x (p_x (right_pt e1)) then let intersection_y := Qred (cross_second_coordinate e1 e2) in Some (Bedge (left_pt e1) (Bpt intersection_x intersection_y), Bedge (Bpt intersection_x intersection_y) (right_pt e1)) else None in let new2 := if Qlt_bool (p_x (left_pt e2)) intersection_x && Qlt_bool intersection_x (p_x (right_pt e2)) then let intersection_y := Qred (cross_second_coordinate e1 e2) in Some (Bedge (left_pt e2) (Bpt intersection_x intersection_y), Bedge (Bpt intersection_x intersection_y) (right_pt e2)) else None in (new1, new2).
imports: Arith QArith List smooth_trajectories Reals