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