theorem :: XREAL_1:74

for a, b, c being Real st 0 < c & a < b holds
a / c < b / c by Lm26;