for x, y, z being ExtReal st x < y & 0 < z & z <> +infty holds
x / z < y / z