let th be real number ; :: thesis: cot (- th) = - (cot th)
cot (- th) = (cos th) / (sin (- th)) by SIN_COS:34
.= (cos th) / (- (sin th)) by SIN_COS:34
.= - (cot th) by XCMPLX_1:189 ;
hence cot (- th) = - (cot th) ; :: thesis: verum