theorem Th75: :: SIN_COS9:75

for r being Real st - 1 <= r & r <= 1 holds
diff (arctan,r) = 1 / (1 + (r ^2))