theorem Th76: :: SIN_COS9:76
for r being Real st - 1 <= r & r <= 1 holds
diff (arccot,r) = - (1 / (1 + (r ^2)))