proposition: Lemma noc14 : let l := List.concat (List.map outgoing evs14) in forallb (fun g => forallb (fun g' => edge_eqb g g' || negb (have_crossing g g')) l) l = true.
proof: Proof. easy. Qed.
imports: Arith QArith List smooth_trajectories Reals