for x being Real st cos x <> 0 holds
sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2))