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 montgomery-mul-of-mod-order (implies (and (montgomery-add-closure) (montgomery-add-associativity) (integerp scalar) (point-on-montgomery-p point curve) (natp order) (montgomery-point-orderp point order curve)) (equal (montgomery-mul (mod scalar order) point curve) (montgomery-mul scalar point curve))))