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