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.
This follows from the definition of having order jubjub-r.
Theorem:
(defthm not-jubjub-r-pointp-when-lower-order (implies (and (jubjub-pointp point) (not (equal point (twisted-edwards-zero))) (posp k) (< k (jubjub-r)) (equal (jubjub-mul k point) (twisted-edwards-zero))) (not (jubjub-r-pointp point))))