A1: for x being Real st x in ].0,PI.[ holds
diff (cot,x) < 0

proof

let x be Real; :: thesis: ( x in ].0,PI.[ implies diff (cot,x) < 0 )
assume A2: x in ].0,PI.[ ; :: thesis: diff (cot,x) < 0
then 0 < sin . x by COMPTRIG:7;
then (sin . x) ^2 > 0 ;
then 1 / ((sin . x) ^2) > 0 / ((sin . x) ^2) ;
then - (1 / ((sin . x) ^2)) < - 0 ;
hence diff (cot,x) < 0 by A2, Lm4; :: thesis: verum

end;

].0,PI.[ c= dom cot by Lm2, FDIFF_1:def 6;
hence cot | ].0,PI.[ is decreasing by A1, Lm2, ROLLE:10; :: thesis: verum