for k being Integer holds 1,k are_coprime