let x, y, n be Integer; :: thesis: ( x,y are_congruent_mod n iff ex k being Integer st x = (k * n) + y )

now :: thesis: ( x,y are_congruent_mod n implies ex k being Integer st x = (k * n) + y )

assume x,y are_congruent_mod n ; :: thesis: ex k being Integer st x = (k * n) + y
then consider k being Integer such that
A1: n * k = x - y ;
x = (n * k) + y by A1;
hence ex k being Integer st x = (k * n) + y ; :: thesis: verum

end;

hence ( x,y are_congruent_mod n iff ex k being Integer st x = (k * n) + y ) ; :: thesis: verum