let m, n, k be Nat; :: thesis: ( 0 < n & m mod n = k implies n divides m - k )
assume A1: ( 0 < n & m mod n = k ) ; :: thesis: n divides m - k
take m div n ; :: according to INT_1:def 3 :: thesis: m - k = n * (m div n)
m = (n * (m div n)) + k by A1, NAT_D:2;
hence m - k = n * (m div n) ; :: thesis: verum