fact: Definition door_right_cell (cells : seq cell) (v : vert_edge) := find (fun i => existsb (fun v' => vert_edge_eqb v v') (cell_safe_exits_left (nth i cells dummy_cell))) (seq.iota 0 (List.length cells)).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL