theorem :: SIN_COS5:19

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