theorem Th73: :: SIN_COS9:73

arctan is_differentiable_on ].(- 1),1.[