let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies cot (arctan r) = 1 / r )
set x = arctan r;
assume that
A1: - 1 <= r and
A2: r <= 1 ; :: thesis: cot (arctan r) = 1 / r
A3: (sin (arctan r)) / (cos (arctan r)) = tan (arctan r) by SIN_COS4:def 1
.= r by A1, A2, Th51 ;
cot (arctan r) = (cos (arctan r)) / (sin (arctan r)) by SIN_COS4:def 2
.= 1 / r by A3, XCMPLX_1:57 ;
hence cot (arctan r) = 1 / r ; :: thesis: verum