Scalar multiplication modulo order.
Multiplication by a scalar is the same as multiplication by the scalar modulo the order of the point. This is for points of non-zero order.
Theorem:
(defthm twisted-edwards-mul-of-mod-order (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point) (integerp scalar) (point-on-twisted-edwards-p point curve) (natp order) (twisted-edwards-point-orderp point order curve)) (equal (twisted-edwards-mul (mod scalar order) point curve) (twisted-edwards-mul scalar point curve))))