Left and right identity properties of the neutral point.
Theorem:
(defthm twisted-edwards-add-of-twisted-edwards-zero-left (implies (point-on-twisted-edwards-p point curve) (equal (twisted-edwards-add (twisted-edwards-zero) point curve) (point-fix point))))
Theorem:
(defthm twisted-edwards-add-of-twisted-edwards-zero-right (implies (point-on-twisted-edwards-p point curve) (equal (twisted-edwards-add point (twisted-edwards-zero) curve) (point-fix point))))