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