Theorem about points on the curve with the same abscissa being the same or opposite points.
If two points on the curve have the same
Theorem:
(defthm montgomery-points-with-same-x-are-same-or-neg-point (implies (and (pointp point1) (pointp point2) (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 point1 point2) (equal point1 (montgomery-neg point2 curve)))))