theorem Th2: :: EULER_1:2
for k, n being Nat st k <> 0 & k < n & n is prime holds
k,n are_coprime