fact: Definition pre_cross_second_coordinate (e1 : edge) (cross_coordinate : Q) := Qred (p_y (left_pt e1) + (p_y (right_pt e1) - p_y (left_pt e1)) / (p_x (right_pt e1) - p_x (left_pt e1)) * (cross_coordinate - p_x (left_pt e1))).
imports: Arith QArith List smooth_trajectories Reals