let th be Real; :: thesis: cot (- th) = - (cot th)
cot (- th) = (cos th) / (sin (- th)) by SIN_COS:31
.= (cos th) / (- (sin th)) by SIN_COS:31
.= - (cot th) by XCMPLX_1:188 ;
hence cot (- th) = - (cot th) ; :: thesis: verum