theorem :: NEWTON06:18

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