Theorem about the only points with zero abscissa or unit ordinate on twisted Edwards curves.
The points
This theorem has some significance, in particular, for the birational equivalence between
Montgomery and twisted Edwards curves: points with
Theorem:
(defthm twisted-edwards-only-points-with-x-0-or-y-1 (b* ((p (twisted-edwards-curve->p curve)) (x (point-finite->x point)) (y (point-finite->y point))) (implies (or (equal x 0) (equal y 1)) (implies (point-on-twisted-edwards-p point curve) (or (equal point (point-finite 0 1)) (equal point (point-finite 0 (neg 1 p))))))))