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