fact: Definition leftmost_points (bottom top : edge) := if p_x (left_pt bottom) [<] p_x (left_pt top) then if vertical_intersection_point (left_pt top) bottom is Some pt then [:: left_pt top; pt] else [::] else if vertical_intersection_point (left_pt bottom) top is Some pt then [:: pt; left_pt bottom] else [::].
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL