fact: Definition close_cell (p : pt) (c : cell) := match vertical_intersection_point p (low c), vertical_intersection_point p (high c) with | None, _ | _, None => c | Some p1, Some p2 => Bcell (left_pts c) (no_dup_seq (p1 :: p :: p2 :: nil)) (low c) (high c) end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL