fact: Fixpoint find_all_crossing_points (e : edge) (evs : seq event) : seq Q := match evs with | nil => nil | Bevent p outg :: evs' => map (fun g => Qred (cross_first_coordinate e g)) (filter (have_crossing e) outg) ++ find_all_crossing_points e evs' end.
imports: Arith QArith List smooth_trajectories Reals