theorem :: XREAL_1:152

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