fact: Definition reverse_step cells cell_i : seq (nat * nat) := map (fun i => (i, cell_i)) (filter (fun c_i => bi_connected (nth c_i cells dummy_cell) (nth cell_i cells dummy_cell)) (seq.iota 0 (List.length cells))).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL