Commutativity of twisted Edwards addition.
Theorem: twisted-edwards-add-commutative
(defthm twisted-edwards-add-commutative (equal (twisted-edwards-add point1 point2 curve) (twisted-edwards-add point2 point1 curve)))