Proof of closure of group addition on a twisted Edwards curve.
We prove that adding two points on a curve always yields a point on the curve. That is, the group operation is closed.
The proof is explained in comments in this file.
Theorem:
(defthm point-on-twisted-edwards-p-of-twisted-edward-add (implies (and (twisted-edwards-curve-completep curve) (pointp point1) (pointp point2) (point-on-twisted-edwards-p point1 curve) (point-on-twisted-edwards-p point2 curve)) (point-on-twisted-edwards-p (twisted-edwards-add point1 point2 curve) curve)))