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