for q being Rational holds numerator q, denominator q are_coprime