source 2008 Bernstein--Lange--Rezaeian-Farashahi "Binary Edwards Curves"
parameter sqrta6
assume sqrta6^2 = a6
compute A = X1^2
compute B = Y1^2
compute Z3 = ZZ1 A
compute ZZ3 = Z3^2
compute X3 = (A+ sqrta6 ZZ1)^2
compute Y3 = B (B + X3 + Z3) + a6 ZZ3 + ZZ3