theorem :: XREAL_1:218

for a being Real st a <= 1 / 2 holds
0 <= 1 - (2 * a)