theorem :: XREAL_1:158

for a, b being Real st a < 0 & 1 < b holds
a * b < a