fact: Definition point_strictly_under_edge (p : pt) (e : edge) : bool := Qlt_bool (pue_formula p (left_pt e) (right_pt e)) 0.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL