theorem :: SIN_COS9:70

for r being Real st - 1 <= r & r <= 1 holds
tan (arccot r) = 1 / r