fact: Fixpoint edges_to_events (s : seq edge) : seq event := match s with | nil => nil | e :: s' => add_event (left_pt e) e false (add_event (right_pt e) e true (edges_to_events s')) end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL