Distributivity of negation over addition.
This says that
This should be provable automatically via suitably normalizing commutativity and associativity rules, but since we do not have them at the moment, we carry out a more manual, step-wise proof. Those rules, and a general form of this theorem, belong to a generic group library anyhow.
Theorem:
(defthm montgmery-neg-of-add (implies (and (montgomery-add-closure) (montgomery-add-associativity) (point-on-montgomery-p point1 curve) (point-on-montgomery-p point2 curve)) (equal (montgomery-neg (montgomery-add point1 point2 curve) curve) (montgomery-add (montgomery-neg point1 curve) (montgomery-neg point2 curve) curve))))