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