Doubling a point is like adding the point to itself.
Theorem: jubjub-mul-of-2
(defthm jubjub-mul-of-2 (implies (jubjub-pointp point) (equal (jubjub-mul 2 point) (jubjub-add point point))))
