for x being Element of RAT+ holds numerator x, denominator x are_coprime