		Search-engine friendly clone of the ACL2 documentation.

Jubjub-r-properties

Jubjub-r-doubling-of-nonzero-is-nonzero

Doubling a non-zero point in jubjub-r-pointp yields a non-zero point.

This is because otherwise the point would have order 2.

Definitions and Theorems

Theorem: jubjub-r-doubling-of-nonzero-is-nonzero

(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)))))