fact: Definition update_closed_cell (c : cell) (p : pt) : cell := let ptseq := right_pts c in let newptseq := (belast (head dummy_pt ptseq) (behead ptseq)) ++ [:: p; seq.last dummy_pt ptseq] in Bcell (left_pts c) newptseq (low c) (high c).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL