theorem :: EULER_2:1

for a, b being Nat holds
( a,b are_coprime iff a,b are_coprime ) ;