for p being Rational holds numerator p = (numerator p) div ((numerator p) gcd (denominator p))