for n, m being Nat holds [\(m / n)/] = m div n ;