theorem Th16: :: EC_PF_1:16

for i being Integer
for p being Prime
for a being Element of (GF p) st a = i mod p holds
- a = (p - i) mod p