fact: Definition edge_determinant (e1 e2 : edge) : Q := let y1 := p_y (right_pt e1) - p_y (left_pt e1) in let x1 := p_x (right_pt e1) - p_x (left_pt e1) in let y2 := p_y (right_pt e2) - p_y (left_pt e2) in let x2 := p_x (right_pt e2) - p_x (left_pt e2) in x1 * y2 - x2 * y1.
imports: Arith QArith List smooth_trajectories Reals