theorem LemacikX1: :: ROUGHIF2:1
for a, b, c being Real st a <= b & b > 0 & c >= 0 holds
a / b <= (a + c) / (b + c)