Injectivity of doubling in jubjub-r-pointp.
This is proved by cases on whether the points are zero or not. The case in which they are both non-zero is the more complicated one:
Theorem:
(defthm jubjub-r-doubling-injectivity (implies (and (ecurve::twisted-edwards-add-associativity) (jubjub-r-pointp x) (jubjub-r-pointp y)) (equal (equal (jubjub-mul 2 x) (jubjub-mul 2 y)) (equal x y))))