:: deftheorem defines cot SIN_COS4:def 2 :
for th being Real holds cot th = (cos th) / (sin th);