let a, b, m be Nat; :: thesis: ( m > 0 implies ( a mod m = b mod m iff m divides a - b ) )
assume A1: m > 0 ; :: thesis: ( a mod m = b mod m iff m divides a - b )
thus ( a mod m = b mod m implies m divides a - b ) :: thesis: ( m divides a - b implies a mod m = b mod m )

proof

assume a mod m = b mod m ; :: thesis: m divides a - b
then (a - b) mod m = 0 by A1, Th22;
hence m divides a - b by A1, INT_1:62; :: thesis: verum

end;

assume m divides a - b ; :: thesis: a mod m = b mod m
then (a - b) mod m = 0 by A1, INT_1:62;
hence a mod m = b mod m by A1, Th22; :: thesis: verum