Doubling a non-zero point in jubjub-r-pointp yields a non-zero point.
This is because otherwise the point would have order 2.
Theorem:
(defthm jubjub-r-doubling-of-nonzero-is-nonzero (implies (and (jubjub-r-pointp point) (not (equal point (twisted-edwards-zero)))) (not (equal (jubjub-mul 2 point) (twisted-edwards-zero)))))