:: deftheorem defines arccot SIN_COS9:def 4 :
for r being Real holds arccot r = arccot . r;