theorem :: COMPTRIG:24

sin | [.(PI / 2),((3 / 2) * PI).] is decreasing