Associativity of scalar multiplication.
This involves heterogeneous entities, namely two scalars and a point. Multiplying the point by one scalar and the the other is equivalent to multiplying the scalars first and then the point.
Theorem:
(defthm twisted-edwards-mul-of-mul (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve) (integerp scalar) (integerp scalar1)) (equal (twisted-edwards-mul scalar (twisted-edwards-mul scalar1 point curve) curve) (twisted-edwards-mul (* scalar scalar1) point curve))))
Theorem:
(defthm twisted-edwards-mul-of-mul-converse (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve) (integerp scalar) (integerp scalar1)) (equal (twisted-edwards-mul (* scalar scalar1) point curve) (twisted-edwards-mul scalar (twisted-edwards-mul scalar1 point curve) curve))))