A non-zero point on a Montgomery curve is finite.
Theorem:
(defthm point-on-montgomery-finite-when-not-zero (implies (and (pointp point) (point-on-montgomery-p point curve) (not (equal point (montgomery-zero)))) (equal (point-kind point) :finite)))