theorem :: SIN_COS2:4

cos | ].0,(PI / 2).[ is decreasing