If adding the same point on the left to two points P1 and P2 yields equal points, then P1 and P2 are equal.
Theorem:
(defthm twisted-edwards-add-cancel-left (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (point-on-twisted-edwards-p point curve) (point-on-twisted-edwards-p point1 curve) (point-on-twisted-edwards-p point2 curve)) (equal (equal (twisted-edwards-add point point1 curve) (twisted-edwards-add point point2 curve)) (equal (point-fix point1) (point-fix point2)))))