theorem :: SIN_COS5:31

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