Negating the ordinate of a point in jubjub-r-pointp yields a point that is not in jubjub-r-pointp.
This is Theorem 5.4.3 in [ZPS]. The proof here follows the one in [ZPS]. It makes use of some of the preceding theorems.
Theorem:
(defthm not-jubjub-r-pointp-of-jubjub-r-point-with-neg-ordinate (implies (and (ecurve::twisted-edwards-add-associativity) (jubjub-r-pointp point)) (not (jubjub-r-pointp (ecurve::point-finite (jubjub-point->u point) (neg (jubjub-point->v point) (jubjub-q)))))))