theorem Th45: :: SIN_COS9:45

arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is increasing