let i, j be Integer; :: thesis: ( i,j are_coprime iff - i, - j are_coprime )
( (- i) gcd j = i gcd j & (- i) gcd j = (- i) gcd (- j) ) by NEWTON02:1;
hence ( i,j are_coprime iff - i, - j are_coprime ) ; :: thesis: verum