theorem :: SINCOS10:118

for r being Real st - (sqrt 2) < r & r < - 1 holds
cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1)))