theorem Th76: :: ARYTM_3:76

for r, s, t being Element of RAT+ holds
( s + t <=' r + t iff s <=' r )