theorem Th100: :: SINCOS10:100
rng (arccosec2 | [.1,(sqrt 2).]) = [.(PI / 4),(PI / 2).]