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