theorem :: XXREAL_3:79

for x, y, z being ExtReal st x <= y & 0 < z holds
x / z <= y / z by Th71;