theorem :: SIN_COS5:10

for x being Real st sin x <> 0 holds
cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x))