theorem :: SIN_COS5:32

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