Theorem about points on the curve with the same abscissa having the same or opposite ordinates.
If two points on the curve have the same
Theorem:
(defthm montgomery-points-with-same-x-have-same-or-neg-y (implies (and (point-on-montgomery-p point1 curve) (point-on-montgomery-p point2 curve) (equal (point-kind point1) :finite) (equal (point-kind point2) :finite) (equal (point-finite->x point1) (point-finite->x point2))) (or (equal (point-finite->y point1) (point-finite->y point2)) (equal (point-finite->y point1) (neg (point-finite->y point2) (montgomery-curve->p curve))))))