let th1, th2 be Real; :: thesis:
(cos th1) - (cos th2) = (cos ((th1 / 2) + (th1 / 2))) - (cos ((th2 / 2) + (th2 / 2)))
.= (((cos (th1 / 2)) * (cos (th1 / 2))) - ((sin (th1 / 2)) * (sin (th1 / 2)))) - (cos ((th2 / 2) + (th2 / 2))) by SIN_COS:75
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + (1 + (- 1))) - (((cos (th2 / 2)) * (cos (th2 / 2))) - ((sin (th2 / 2)) * (sin (th2 / 2)))) by SIN_COS:75
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + 1) + ((- 1) + ((- ((cos (th2 / 2)) * (cos (th2 / 2)))) + ((sin (th2 / 2)) * (sin (th2 / 2)))))
.= ((((cos (th1 / 2)) * (cos (th1 / 2))) + (- ((sin (th1 / 2)) * (sin (th1 / 2))))) + (((sin (th1 / 2)) * (sin (th1 / 2))) + ((cos (th1 / 2)) * (cos (th1 / 2))))) + ((- 1) + ((- ((cos (th2 / 2)) * (cos (th2 / 2)))) + ((sin (th2 / 2)) * (sin (th2 / 2))))) by SIN_COS:29
.= (((cos (th1 / 2)) * (cos (th1 / 2))) + ((((sin (th1 / 2)) * (sin (th1 / 2))) - (- (- ((sin (th1 / 2)) * (sin (th1 / 2)))))) + ((cos (th1 / 2)) * (cos (th1 / 2))))) + ((- (((sin (th2 / 2)) * (sin (th2 / 2))) + ((cos (th2 / 2)) * (cos (th2 / 2))))) + ((- ((cos (th2 / 2)) * (cos (th2 / 2)))) + ((sin (th2 / 2)) * (sin (th2 / 2))))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * 1) - ((cos (th2 / 2)) * (cos (th2 / 2))))
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * (((sin (th2 / 2)) * (sin (th2 / 2))) + ((cos (th2 / 2)) * (cos (th2 / 2))))) - ((cos (th2 / 2)) * (cos (th2 / 2)))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * ((sin (th2 / 2)) * (sin (th2 / 2)))) + (((cos (th2 / 2)) * (cos (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) - (- (- 1)))))
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * ((sin (th2 / 2)) * (sin (th2 / 2)))) + (((cos (th2 / 2)) * (cos (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) - (- (- (((cos (th1 / 2)) * (cos (th1 / 2))) + ((sin (th1 / 2)) * (sin (th1 / 2))))))))) by SIN_COS:29
.= - (2 * ((((sin (th1 / 2)) * (cos (th2 / 2))) - (- (- ((cos (th1 / 2)) * (sin (th2 / 2)))))) * (((sin (th1 / 2)) * (cos (th2 / 2))) + ((cos (th1 / 2)) * (sin (th2 / 2))))))
.= - (2 * ((sin ((th1 / 2) + (th2 / 2))) * (((sin (th1 / 2)) * (cos (th2 / 2))) - ((cos (th1 / 2)) * (sin (th2 / 2)))))) by SIN_COS:75
.= - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 / 2) - (th2 / 2))))) by SIN_COS:82
.= - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) ;
hence (cos th1) - (cos th2) = - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2)))) ; :: thesis: