theorem :: XREAL_1:236

for a, b, c being Real st a <= b & c < a holds
b -' a < b -' c