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))) - (((sin (th2 / 2)) * (sin (th2 / 2))) * 1))
.= 2 * (((cos (th1 / 2)) * (cos (th1 / 2))) - (((sin (th2 / 2)) * (sin (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) + ((sin (th1 / 2)) * (sin (th1 / 2)))))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * (1 - (- (- ((sin (th2 / 2)) * (sin (th2 / 2))))))) + (- (((sin (th2 / 2)) * (sin (th2 / 2))) * ((sin (th1 / 2)) * (sin (th1 / 2))))))
.= 2 * ((((cos (th1 / 2)) * (cos (th1 / 2))) * ((((cos (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (sin (th2 / 2)))) - (- (- ((sin (th2 / 2)) * (sin (th2 / 2))))))) + (- (((sin (th2 / 2)) * (sin (th2 / 2))) * ((sin (th1 / 2)) * (sin (th1 / 2)))))) by SIN_COS:29
.= 2 * ((((cos (th1 / 2)) * (cos (th2 / 2))) + ((sin (th1 / 2)) * (sin (th2 / 2)))) * (((cos (th1 / 2)) * (cos (th2 / 2))) + (- ((sin (th1 / 2)) * (sin (th2 / 2))))))
.= 2 * ((cos ((th1 / 2) - (th2 / 2))) * (((cos (th1 / 2)) * (cos (th2 / 2))) - ((sin (th1 / 2)) * (sin (th2 / 2))))) by SIN_COS:83
.= 2 * ((cos ((th1 - th2) / 2)) * (cos ((th1 / 2) + (th2 / 2)))) by SIN_COS:75
.= 2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2))) ;
hence (cos th1) + (cos th2) = 2 * ((cos ((th1 + th2) / 2)) * (cos ((th1 - th2) / 2))) ; :: thesis: