for x being Real st x in ].0,PI.[ holds
cot . x = cot x