fact: Fixpoint add_event (p : pt) (e : edge) (inc : bool) (evs : seq event) : seq event := match evs with | nil => if inc then (Bevent p nil :: nil) else (Bevent p (e :: nil) :: nil) | ev1 :: evs' => let p1 := point ev1 in if pt_eqb p p1 then if inc then Bevent p1 (outgoing ev1) :: evs' else Bevent p1 (e :: outgoing ev1) :: evs' else if Qlt_bool (p_x p) (p_x p1) then if inc then Bevent p nil :: evs else Bevent p (e :: nil) :: evs else if Qeq_bool (p_x p) (p_x p1) && Qlt_bool (p_y p) (p_y p1) then if inc then Bevent p nil :: evs else Bevent p (e :: nil) :: evs else ev1 :: add_event p e inc evs' end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL