fact: Definition start (first_event : event) (bottom : edge) (top : edge) : scan_state := let (newcells, lastopen) := opening_cells_aux (point first_event) (path.sort edge_below (outgoing first_event)) bottom top in (Bscan newcells lastopen [::] [::] (close_cell (point first_event) (start_open_cell bottom top)) top (p_x (point first_event))).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL