theorem Th16: :: SINCOS10:16
cosec | ].0,(PI / 2).[ is decreasing