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