theorem Th123: :: SINCOS10:123

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