theorem Th121: :: SINCOS10:121

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