let x be Real; :: thesis: coth (- x) = - (coth x)
coth (- x) = (cosh . (- x)) / (sinh (- x)) by SIN_COS2:def 4
.= (cosh . (- x)) / (sinh . (- x)) by SIN_COS2:def 2
.= (cosh . x) / (sinh . (- x)) by SIN_COS2:19
.= (cosh . x) / (- (sinh . x)) by SIN_COS2:19
.= - ((cosh . x) / (sinh . x)) by XCMPLX_1:188
.= - ((cosh x) / (sinh . x)) by SIN_COS2:def 4
.= - (coth x) by SIN_COS2:def 2 ;
hence coth (- x) = - (coth x) ; :: thesis: verum