theorem NDD: :: NUMERAL3:91

for a being Rational holds [\a/] = (numerator a) div (denominator a)