theorem Th26: :: EC_PF_2:26

for p being Prime
for g2, a, b being Element of (GF p) st g2 = 2 mod p holds
(a - b) |^ 2 = ((a |^ 2) - ((g2 * a) * b)) + (b |^ 2)