theorem Th124: :: SINCOS10:124

arccosec2 is_differentiable_on cosec .: ].0,(PI / 2).[