for n, m being Nat st 0 < m holds
n mod m = n - (m * (n div m))