Jubjub-point-abscissa-is-not-1
A Jubjub point cannot have abscissa 1.
The reason is that, if we set u = 1 in the curve equation,
we obtain that v^2 is equal to the non-square (1-a)/(1-d),
an impossibility (the fact that (1-a)/(1-d), which has a known value,
is not a square, can be seen using Euler's criterion.
A more detailed proof is in Theorem 5.4.5 in [ZPS:5.4.8.2].
Definitions and Theorems
Theorem: jubjub-point-abscissa-is-not-1
(defthm jubjub-point-abscissa-is-not-1
(implies (jubjub-pointp point)
(not (equal (jubjub-point->u point) 1))))
