fact: Definition cross_second_coordinate (e1 e2 : edge) := if Qeq_bool (p_x (left_pt e1)) (p_x (right_pt e1)) then pre_cross_second_coordinate e2 (cross_first_coordinate e1 e2) else pre_cross_second_coordinate e1 (cross_first_coordinate e1 e2).
imports: Arith QArith List smooth_trajectories Reals