|
|
|---|
|
|
|
|---|
If a point has a certain order, its negation has the same order.
The key property used here is that the multiplication of a negated point is the same as the negation of the multiplied point.
Theorem:
(defthm twisted-edwards-point-orderp-of-neg (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve) (natp order) (twisted-edwards-point-orderp point order curve)) (twisted-edwards-point-orderp (twisted-edwards-neg point curve) order curve)))