Multiplying a Montgomery point by two distinct and not opposite non-zero scalars in the range of the point order yields points with distinct abscissae.
This is essentially Theorem A.3.4 in the Zcash Protocol Specification (Version 2020.1.15), without the hypothesis that the order of the point is odd, which is not needed to prove the fact that the abscissae are distinct.
Theorem:
(defthm montgomery-distinct-x-when-nonzero-mul-in-order-range (implies (and (montgomery-add-closure) (montgomery-add-associativity) (point-on-montgomery-p point curve) (natp order) (montgomery-point-orderp point order curve) (integerp k1) (or (and (<= (- (/ (1- order) 2)) k1) (< k1 0)) (and (< 0 k1) (<= k1 (/ (1- order) 2)))) (equal point1 (montgomery-mul k1 point curve)) (integerp k2) (or (and (<= (- (/ (1- order) 2)) k2) (< k2 0)) (and (< 0 k2) (<= k2 (/ (1- order) 2)))) (equal point2 (montgomery-mul k2 point curve)) (not (equal k1 k2)) (not (equal k1 (- k2)))) (and (equal (point-kind point1) :finite) (equal (point-kind point2) :finite) (not (equal (point-finite->x point1) (point-finite->x point2))))))