theorem :: XREAL_1:174

for a, b, c, d being Real st 0 <= d & d <= 1 & b <= a & c <= a holds
((1 - d) * b) + (d * c) <= a