let m, n be Nat; :: thesis: ( 0 < m implies n mod m = n - (m * (n div m)) )
assume A1: m > 0 ; :: thesis: n mod m = n - (m * (n div m))
reconsider z1 = m * (n div m), z2 = n mod m as Integer ;
n - z1 = (z1 + z2) - z1 by A1, NAT_D:2;
hence n mod m = n - (m * (n div m)) ; :: thesis: verum