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