let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies diff (arccot,r) = - (1 / (1 + (r ^2))) )
set g = arccot ;
set f = cot | ].0,PI.[;
set x = arccot . r;
assume that
A1: - 1 <= r and
A2: r <= 1 ; :: thesis: diff (arccot,r) = - (1 / (1 + (r ^2)))
A3: ((sin . (arccot . r)) ^2) + ((cos . (arccot . r)) ^2) = 1 by SIN_COS:28;
A4: cot | ].0,PI.[ is_differentiable_on ].0,PI.[ by Lm2, FDIFF_2:16;

A5: now :: thesis: for x0 being Real st x0 in ].0,PI.[ holds
diff ((cot | ].0,PI.[),x0) < 0

A6: for x0 being Real st x0 in ].0,PI.[ holds
- (1 / ((sin . x0) ^2)) < 0

proof

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

end;

let x0 be Real; :: thesis: ( x0 in ].0,PI.[ implies diff ((cot | ].0,PI.[),x0) < 0 )
assume A7: x0 in ].0,PI.[ ; :: thesis: diff ((cot | ].0,PI.[),x0) < 0
diff ((cot | ].0,PI.[),x0) = ((cot | ].0,PI.[) `| ].0,PI.[) . x0 by A4, A7, FDIFF_1:def 7
.= (cot `| ].0,PI.[) . x0 by Lm2, FDIFF_2:16
.= diff (cot,x0) by A7, Lm2, FDIFF_1:def 7
.= - (1 / ((sin . x0) ^2)) by A7, Lm4 ;
hence diff ((cot | ].0,PI.[),x0) < 0 by A7, A6; :: thesis: verum

end;

A8: r in [.(- 1),1.] by A1, A2, XXREAL_1:1;
then A9: arccot . r in [.(PI / 4),((3 / 4) * PI).] by Th50;
arccot . r = arccot r ;
then A10: r = cot (arccot . r) by A1, A2, Th52
.= (cos (arccot . r)) / (sin (arccot . r)) by SIN_COS4:def 2 ;
dom (cot | ].0,PI.[) = (dom cot) /\ ].0,PI.[ by RELAT_1:61;
then A11: ].0,PI.[ c= dom (cot | ].0,PI.[) by Th2, XBOOLE_1:19;
A12: (cot | ].0,PI.[) | ].0,PI.[ = cot | ].0,PI.[ by RELAT_1:72;
A13: [.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[ by Lm9, Lm10, XXREAL_2:def 12;
then sin (arccot . r) <> 0 by A9, COMPTRIG:7;
then r * (sin (arccot . r)) = cos (arccot . r) by A10, XCMPLX_1:87;
then A14: 1 = ((sin (arccot . r)) ^2) * ((r ^2) + 1) by A3;
cot | ].0,PI.[ is_differentiable_on ].0,PI.[ by Lm2, FDIFF_2:16;
then diff ((cot | ].0,PI.[),(arccot . r)) = ((cot | ].0,PI.[) `| ].0,PI.[) . (arccot . r) by A9, A13, FDIFF_1:def 7
.= (cot `| ].0,PI.[) . (arccot . r) by Lm2, FDIFF_2:16
.= diff (cot,(arccot . r)) by A9, A13, Lm2, FDIFF_1:def 7
.= - (1 / ((sin (arccot . r)) ^2)) by A9, A13, Lm4 ;
then diff (arccot,r) = 1 / (- (1 / ((sin (arccot . r)) ^2))) by A8, A4, A5, A12, A11, Th24, FDIFF_2:48
.= - (1 / (1 / ((sin (arccot . r)) ^2))) by XCMPLX_1:188
.= - (1 / ((r ^2) + 1)) by A14, XCMPLX_1:73 ;
hence diff (arccot,r) = - (1 / (1 + (r ^2))) ; :: thesis: verum