		Search-engine friendly clone of the ACL2 documentation.

Jubjub-r-properties

Properties about jubjub-r-pointp.

Not-jubjub-r-pointp-when-0-ordinate: A Jubjub point with 0 ordinate is not in jubjub-r-pointp.
Jubjub-r-doubling-injectivity: Injectivity of doubling in jubjub-r-pointp.
Point-0-m1: The point (0,-1).
Not-jubjub-r-pointp-of-jubjub-r-point-with-neg-ordinate: Negating the ordinate of a point in jubjub-r-pointp yields a point that is not in jubjub-r-pointp.
Not-jubjub-r-pointp-when-lower-order: If multiplying a non-zero point by a positive integer below jubjub-r yields the zero point, the non-zero point is not in jubjub-r-pointp.
Jubjub-r-doubling-of-nonzero-is-nonzero: Doubling a non-zero point in jubjub-r-pointp yields a non-zero point.
Jubjub-point->u-injective-on-jubjub-r-pointp: jubjub-point->u is injective in jubjub-r-pointp.