theorem :: SINCOS10:12
cosec | ].0,(PI / 2).[ is continuous by Th8, FDIFF_1:25;