theorem :: NEWTON06:20

for a being positive Real st 1 / 2 < frac a holds
frac (2 * a) < frac a