Uniqueness of inverse (i.e. negation).
If adding a point
Theorem:
(defthm twisted-edwards-add-zero-left-is-neg (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point1) (pointp point2) (point-on-twisted-edwards-p point1 curve) (point-on-twisted-edwards-p point2 curve)) (equal (equal (twisted-edwards-add point1 point2 curve) (twisted-edwards-zero)) (equal point1 (twisted-edwards-neg point2 curve)))))
Theorem:
(defthm twisted-edwards-add-zero-right-is-neg (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point1) (pointp point2) (point-on-twisted-edwards-p point1 curve) (point-on-twisted-edwards-p point2 curve)) (equal (equal (twisted-edwards-add point1 point2 curve) (twisted-edwards-zero)) (equal point2 (twisted-edwards-neg point1 curve)))))