theorem :: XREAL_1:217

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