let x be Real; :: thesis: 1 + (cos (2 * x)) = 2 * ((cos x) ^2)
1 + (cos (2 * x)) = 1 + (cos (x + x))
.= 1 + (((cos x) ^2) - ((sin x) ^2)) by SIN_COS:75
.= (((cos x) ^2) + ((sin x) ^2)) + (((cos x) ^2) - ((sin x) ^2)) by SIN_COS:29
.= 2 * ((cos x) ^2) ;
hence 1 + (cos (2 * x)) = 2 * ((cos x) ^2) ; :: thesis: verum