theorem Th6: :: REAL_3:6

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