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