fact: Definition all_doors (cells : seq cell) : seq (vert_edge * nat) := List.concat (List.map (fun i => List.map (fun v => (v, i)) (cell_safe_exits_right (nth i cells dummy_cell))) (seq.iota 0 (List.length cells))).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL