theorem :: SIN_COS4:9

for th1, th2 being Real st sin th1 <> 0 & sin th2 <> 0 holds
cot (th1 + th2) = (((cot th1) * (cot th2)) - 1) / ((cot th2) + (cot th1))