theorem Th1: :: EULER_1:1

for n being Nat holds
( n,n are_coprime iff n = 1 )