fact: Definition have_crossing (e1 e2 : edge) : bool := let x1 := p_x (right_pt e1) - p_x (left_pt e1) in let d2 := edge_determinant e1 e2 in if Qeq_bool x1 0 then Qlt_bool (p_x (left_pt e2)) (p_x (left_pt e1)) && Qlt_bool (p_x (left_pt e1)) (p_x (right_pt e2)) else if negb (Qeq_bool d2 0) then (Qlt_bool (p_x (left_pt e2)) (cross_first_coordinate e1 e2) && Qlt_bool (cross_first_coordinate e1 e2) (p_x (right_pt e2))) || (Qlt_bool (p_x (left_pt e1)) (cross_first_coordinate e1 e2) && Qlt_bool (cross_first_coordinate e1 e2) (p_x (right_pt e1))) else if negb (Qeq_bool (pue_formula (left_pt e1) (left_pt e2) (right_pt e2)) 0) then true else (Qlt_bool (p_x (left_pt e2)) (p_x (left_pt e1)) && Qlt_bool (p_x (left_pt e1)) (p_x (right_pt e2))) || (Qlt_bool (p_x (left_pt e2)) (p_x (right_pt e1)) && Qlt_bool (p_x (right_pt e1)) (p_x (right_pt e2))) || (Qlt_bool (p_x (left_pt e1)) (p_x (left_pt e2)) && Qlt_bool (p_x (left_pt e2)) (p_x (right_pt e1))) || (Qlt_bool (p_x (left_pt e1)) (p_x (right_pt e2)) && Qlt_bool (p_x (right_pt e2)) (p_x (right_pt e1))).
imports: Arith QArith List smooth_trajectories Reals