theorem :: SIN_COS2:5

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