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:80
.= (((cos x) ^2 ) + ((sin x) ^2 )) + (((cos x) ^2 ) - ((sin x) ^2 )) by SIN_COS:32
.= 2 * ((cos x) ^2 ) ;
hence 1 + (cos (2 * x)) = 2 * ((cos x) ^2 ) ; :: thesis: verum