let x, y, n be Nat; :: thesis: ( n > 0 & x >= y implies ( x,y are_congruent_mod n iff ex k being Nat st x = (k * n) + y ) )
assume A1: n > 0 ; :: thesis: ( not x >= y or ( x,y are_congruent_mod n iff ex k being Nat st x = (k * n) + y ) )
assume x >= y ; :: thesis: ( x,y are_congruent_mod n iff ex k being Nat st x = (k * n) + y )
then A2: x - y >= y - y by XREAL_1:9;

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

assume x,y are_congruent_mod n ; :: thesis: ex k being Nat st x = (k * n) + y
then consider k being Integer such that
A3: n * k = x - y ;
( k >= 0 or n <= 0 ) by A2, A3;
then k in NAT by A1, INT_1:3;
then reconsider k = k as Nat ;
take k = k; :: thesis: x = (k * n) + y
thus x = (k * n) + y by A3; :: thesis: verum

end;

thus ( ex k being Nat st x = (k * n) + y implies x,y are_congruent_mod n ) ; :: thesis: verum