theorem gcdp: :: FIELD_15:3

for p being Prime
for n being non zero Nat st n < p holds
n gcd p = 1