for x being Real st sin . x <> 0 holds
cot . x = cot x