fact: Definition strict_inside_closed p c := negb (point_under_edge p (low c)) && point_strictly_under_edge p (high c) && (Qlt_bool (left_limit c) (p_x p) && (Qlt_bool (p_x p) (right_limit c))).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL