theorem :: NEWTON06:19

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