:: deftheorem defines arctan SIN_COS9:def 3 :
for r being Real holds arctan r = arctan . r;