theorem Th71: :: SIN_COS9:71

arctan is_differentiable_on tan .: ].(- (PI / 2)),(PI / 2).[