theorem :: REAL_3:3

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