theorem Th122: :: SINCOS10:122

arcsec2 is_differentiable_on sec .: ].(PI / 2),PI.[