:: deftheorem defines cot SIN_COS:def 27 :
cot = cos / sin;