for n, m being Nat holds frac (m / n) = (m mod n) / n