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