theorem :: SIN_COS5:12

for x being Real holds cot x = 1 / (tan x) by XCMPLX_1:57;