theorem :: XREAL_1:154

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