ArithOps (N):[Table of Contents] [Index]trait% Defines operators div and mod relative to + and * % for positive denominatorsassumesTotalOrder (N)includesMultiplication (N)introducesdiv, mod: N, N -> Nassertsforallx, y: N y > 0 => (0 <= mod(x, y) /\ mod(x, y) < y /\ (mod(x, y) + (div(x, y) * y)) = x)