for a, b, c being Real st a <= b & c <= 0 holds
b * c <= a * c by Lm28;