theorem Th25: :: SIN_COS9:25

arctan | [.(- 1),1.] = (tan | [.(- (PI / 4)),(PI / 4).]) "