fact: Definition open_cells_decomposition (open_cells : seq cell) (p : pt) : seq cell * seq cell * cell * seq cell * edge * edge := let '(fc, cc, c', lc) := open_cells_decomposition_rec open_cells p in (fc, cc, c', lc, low (head c' cc), high c').
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL