jubjub-point->u is injective in jubjub-r-pointp.
This is Theorem 5.4.4 in [ZPS]. This ACL2 proof follows the proof in [ZPS].
Theorem:
(defthm jubjub-point->u-injective-on-jubjub-r-pointp (implies (and (ecurve::twisted-edwards-add-associativity) (jubjub-r-pointp point) (jubjub-r-pointp qoint)) (equal (equal (jubjub-point->u point) (jubjub-point->u qoint)) (equal point qoint))))