theorem :: SINCOS10:120
for r being Real st 1 < r & r < sqrt 2 holds
sec . (arccosec2 r) = r / (sqrt ((r ^2) - 1))