let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies arccot r = PI - (arccot (- r)) )
set x = arccot (- r);
assume A1: ( - 1 <= r & r <= 1 ) ; :: thesis: arccot r = PI - (arccot (- r))
A2: ( - (- 1) >= - r & - r >= - 1 ) by A1, XREAL_1:26;
then - r in [.(- 1),1.] by XXREAL_1:1;
then A3: arccot (- r) in [.(PI / 4),((3 / 4) * PI ).] by Th48;
- r = cot (arccot (- r)) by A2, Th50;
then A6: r = - (cot (arccot (- r)))
.= - ((cos (arccot (- r))) / (sin (arccot (- r)))) by SIN_COS4:def 2
.= (cos (arccot (- r))) / (- (sin (arccot (- r)))) by XCMPLX_1:189
.= (cos (arccot (- r))) / (sin (- (arccot (- r)))) by SIN_COS:34
.= (cos (- (arccot (- r)))) / (sin (- (arccot (- r)))) by SIN_COS:34
.= cot (- (arccot (- r))) by SIN_COS4:def 2 ;
A7: ( 0 < PI + (- (arccot (- r))) & PI + (- (arccot (- r))) < PI )

proof

( PI / 4 <= arccot (- r) & arccot (- r) <= (3 / 4) * PI ) by A3, XXREAL_1:1;
then ( - (PI / 4) >= - (arccot (- r)) & - (arccot (- r)) >= - ((3 / 4) * PI ) ) by XREAL_1:26;
then ( PI + (- (PI / 4)) >= PI + (- (arccot (- r))) & PI + (- (arccot (- r))) >= PI + (- ((3 / 4) * PI )) ) by XREAL_1:8;
then A8: PI + (- (arccot (- r))) in [.(PI / 4),((3 / 4) * PI ).] by XXREAL_1:1;
[.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
hence ( 0 < PI + (- (arccot (- r))) & PI + (- (arccot (- r))) < PI ) by A8, XXREAL_1:4; :: thesis: verum

end;

cot (PI + (- (arccot (- r)))) = (cos (PI + (- (arccot (- r))))) / (sin (PI + (- (arccot (- r))))) by SIN_COS4:def 2
.= (- (cos (- (arccot (- r))))) / (sin (PI + (- (arccot (- r))))) by SIN_COS:84
.= (- (cos (- (arccot (- r))))) / (- (sin (- (arccot (- r))))) by SIN_COS:84
.= (cos (- (arccot (- r)))) / (sin (- (arccot (- r)))) by XCMPLX_1:192
.= cot (- (arccot (- r))) by SIN_COS4:def 2 ;
hence arccot r = PI - (arccot (- r)) by A6, A7, Th34; :: thesis: verum