theorem :: EULER_2:23

for m, n being Nat holds
( m,n are_coprime iff for k being Nat st k divides m & k divides n holds
k = 1 ) by NOW;