let x, y, n be Integer; ( x,n are_coprime & x,y are_congruent_mod n implies y,n are_coprime )
assume that
A1:
x,n are_coprime
and
A2:
x,y are_congruent_mod n
and
A3:
not y,n are_coprime
; contradiction
consider z being Integer such that
A4:
n * z = x - y
by A2, INT_1:def 5;
set gcdyn = y gcd n;
A5:
y gcd n divides y
by INT_2:21;
A6:
y gcd n divides n
by INT_2:21;
y gcd n divides n * z
by INT_2:2, INT_2:21;
then
y gcd n divides (n * z) + y
by A5, WSIERP_1:4;
then
y gcd n divides x gcd n
by A4, A6, INT_2:22;
then
y gcd n divides 1
by A1, INT_2:def 3;
then A7:
( y gcd n = 1 or y gcd n = - 1 )
by INT_2:13;
0 <= y gcd n
;
hence
contradiction
by A3, A7, INT_2:def 3; verum