theorem :: RAT_1:34

for p being Rational holds
( p <= - 1 iff denominator p <= - (numerator p) )