Multiplying a negated point is like negating the multiplied point.
Theorem:
(defthm twisted-edwards-mul-of-neg (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve) (integerp scalar)) (equal (twisted-edwards-mul scalar (twisted-edwards-neg point curve) curve) (twisted-edwards-neg (twisted-edwards-mul scalar point curve) curve))))