Distributivity of scalar multiplication over scalar addition.
We first prove it on montgomery-mul-nonneg by induction, then we lift it to montgomery-mul, but only for non-negative scalars. To extend it to negative scalars, we consider different cases. If both scalars are non-positive, the definition of montgomery-mul is expanded, and the theorem about montgomery-mul-nonneg applies. If one is non-negative and the other non-positive, we consider two subcases: when the sum is non-negative, and when the sum is non-positive. The first subcase requires adding and subtracting the same quantity, and thus we use Isar to explicate this proof strategy. The second subcase is proved by considering the negated scalars and thus applying the theorem for the first subcase; we use Isar, but it might be possible to shorten the proof. Finally, the case in which one is non-positive and the other non-negative is handled by swapping the roles, and implicitly using commutativity. With all the cases in hand, we prove the main theorem, which applies to any integer scalars. We keep the theorem disabled, because distribution is not always desired.
Note that we consider non-negative and non-positive cases, which overlap at zero, rather than non-overlapping non-negative and negative cases. The overlap is intentional, so that the cases are more symmetric and it is easy to swap signs, as we do in some of the proofs.
Theorem:
(defthm montgomery-mul-of-scalar-addition (implies (and (montgomery-add-closure) (montgomery-add-associativity) (point-on-montgomery-p point curve) (integerp scalar1) (integerp scalar2)) (equal (montgomery-mul (+ scalar1 scalar2) point curve) (montgomery-add (montgomery-mul scalar1 point curve) (montgomery-mul scalar2 point curve) curve))))
Theorem:
(defthm montgomery-mul-of-scalar-addition-converse (implies (and (montgomery-add-closure) (montgomery-add-associativity) (point-on-montgomery-p point curve) (integerp scalar1) (integerp scalar2)) (equal (montgomery-add (montgomery-mul scalar1 point curve) (montgomery-mul scalar2 point curve) curve) (montgomery-mul (+ scalar1 scalar2) point curve))))