fact: Definition inside_box (p : pt) (bottom top : edge) := negb (point_under_edge p bottom) && point_strictly_under_edge p top && (Qlt_bool (p_x (left_pt bottom)) (p_x p) && Qlt_bool (p_x p) (p_x (right_pt bottom))) && (Qlt_bool (p_x (left_pt top)) (p_x p) && Qlt_bool (p_x p) (p_x (right_pt top))).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL