for th being Real st th in ].(PI / 2),PI.[ holds
diff (cos,th) < 0

proof

let th be Real; :: thesis: ( th in ].(PI / 2),PI.[ implies diff (cos,th) < 0 )
assume A1: th in ].(PI / 2),PI.[ ; :: thesis: diff (cos,th) < 0
then th < PI by XXREAL_1:4;
then A2: th - (PI / 2) < PI - (PI / 2) by XREAL_1:9;
PI / 2 < th by A1, XXREAL_1:4;
then (PI / 2) - (PI / 2) < th - (PI / 2) by XREAL_1:9;
then th - (PI / 2) in ].0,(PI / 2).[ by A2, XXREAL_1:4;
then cos . (th - (PI / 2)) > 0 by SIN_COS:80;
then A3: 0 - (cos . (th - (PI / 2))) < 0 ;
diff (cos,th) = - (sin . ((PI / 2) + (th - (PI / 2)))) by SIN_COS:67
.= - (cos . (th - (PI / 2))) by SIN_COS:78 ;
hence diff (cos,th) < 0 by A3; :: thesis: verum

end;

hence cos | ].(PI / 2),PI.[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:67; :: thesis: verum